# HG changeset patch
# User paulson
# Date 948447940 -3600
# Node ID 1e4cb069b19d7367bc7208262d323170493446d5
# Parent  fb6fe34060ca7074c443b90f217547c2cac7ea49
new theorem inj_on_restrict_eq

diff -r fb6fe34060ca -r 1e4cb069b19d src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Thu Jan 20 17:57:59 2000 +0100
+++ b/src/HOL/Fun.ML	Fri Jan 21 10:45:40 2000 +0100
@@ -380,6 +380,7 @@
 by Auto_tac;
 val Pi_extensionality = ballI RSN (3, result());
 
+
 (*** compose ***)
 
 Goalw [Pi_def, compose_def, restrict_def]
@@ -406,7 +407,6 @@
 	      simpset() addsimps [image_def, compose_eq]));
 qed "surj_compose";
 
-
 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(),
@@ -415,7 +415,8 @@
 
 
 (*** restrict / lam ***)
-Goal "[| f `` A <= B |] ==> (lam x: A. f x) : A funcset B";
+
+Goal "f``A <= B ==> (lam x: A. f x) : A funcset B";
 by (auto_tac (claset(),
 	      simpset() addsimps [restrict_def, Pi_def]));
 qed "restrict_in_funcset";
@@ -425,7 +426,6 @@
 by (asm_simp_tac (simpset() addsimps prems) 1);
 qed "restrictI";
 
-
 Goal "x: A ==> (lam y: A. f y) x = f x";
 by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
 qed "restrict_apply1";
@@ -438,7 +438,6 @@
 by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
 qed "restrict_apply2";
 
-
 val prems = Goal
     "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
 by (rtac ext 1);
@@ -446,6 +445,10 @@
 	      simpset() addsimps prems@[restrict_def, Pi_def]));
 qed "restrict_ext";
 
+Goalw [inj_on_def, restrict_def] "inj_on (restrict f A) A = inj_on f A";
+by Auto_tac;
+qed "inj_on_restrict_eq";
+
 
 (*** Inverse ***)