# HG changeset patch # User blanchet # Date 1347438960 -7200 # Node ID a063a96c866206640bae2c997becdcbbaa55bd18 # Parent 340844cbf7af15e990286ab20f2e7fcd6768e284 got rid of metis calls diff -r 340844cbf7af -r a063a96c8662 src/HOL/Codatatype/BNF_LFP.thy --- a/src/HOL/Codatatype/BNF_LFP.thy Wed Sep 12 10:35:56 2012 +0200 +++ b/src/HOL/Codatatype/BNF_LFP.thy Wed Sep 12 10:36:00 2012 +0200 @@ -61,7 +61,8 @@ then obtain g where g: "ALL b : B. g b : A \ f (g b) = b" using bchoice[of B ?phi] by blast hence gg: "ALL b : f ` A. g b : A \ f (g b) = b" using f by blast - have gf: "inver g f A" unfolding inver_def by (metis gg imageI inj_f the_inv_into_f_f) + have gf: "inver g f A" unfolding inver_def + by (metis (no_types) gg imageI[of _ A f] the_inv_into_f_f[OF inj_f]) moreover have "g ` B \ A \ inver f g B" using g unfolding inver_def by blast moreover have "A \ g ` B" proof safe @@ -123,13 +124,16 @@ unfolding bij_betw_def inver_def by auto lemma bij_betwI: "\bij_betw g B A; inver g f A; inver f g B\ \ bij_betw f A B" -by (metis bij_betw_iff_ex bij_betw_imageE) +by (drule bij_betw_imageE, unfold bij_betw_iff_ex) blast lemma bij_betwI': "\\x y. \x \ X; y \ X\ \ (f x = f y) = (x = y); \x. x \ X \ f x \ Y; \y. y \ Y \ \x \ X. y = f x\ \ bij_betw f X Y" -unfolding bij_betw_def inj_on_def by auto (metis rev_image_eqI) +unfolding bij_betw_def inj_on_def +apply (rule conjI) + apply blast +by (erule thin_rl) blast lemma surj_fun_eq: assumes surj_on: "f ` X = UNIV" and eq_on: "\x \ X. (g1 o f) x = (g2 o f) x" @@ -192,7 +196,15 @@ then obtain y where y: "y \ Field r" "\x \ X. (x \ y \ (x, y) \ r)" by blast then obtain z where z: "z \ Field r" "x \ z \ (x, z) \ r" "y \ z \ (y, z) \ r" using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast - show ?case by (metis Card_order_trans insert(5) insertE y(2) z) + show ?case + apply (intro bexI ballI) + apply (erule insertE) + apply hypsubst + apply (rule z(2)) + using Card_order_trans[OF insert(5)[THEN conjunct2]] y(2) z(3) + apply blast + apply (rule z(1)) + done qed lemma insert_subsetI: "\x \ A; X \ A\ \ insert x X \ A"