new constant same_fst

--- a/src/HOL/WF_Rel.ML	Tue Jul 25 01:27:36 2000 +0200
+++ b/src/HOL/WF_Rel.ML	Tue Jul 25 09:48:39 2000 +0200
@@ -208,3 +208,19 @@
 by (asm_simp_tac (simpset() addsimps [le_eq]) 1);
 by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1));
 qed "weak_decr_stable";
+
+(*----------------------------------------------------------------------------
+ * Wellfoundedness of same_fst
+ *---------------------------------------------------------------------------*)
+
+val prems = goalw thy [same_fst_def]
+  "(!!x. P x ==> wf(R x)) ==> wf(same_fst P R)";
+by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1);
+by(strip_tac 1);
+by(rename_tac "a b" 1);
+by(case_tac "wf(R a)" 1);
+ by (eres_inst_tac [("a","b")] wf_induct 1);
+ by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs prems) 1);
+qed "wf_same_fstI";

--- a/src/HOL/WF_Rel.thy	Tue Jul 25 01:27:36 2000 +0200
+++ b/src/HOL/WF_Rel.thy	Tue Jul 25 09:48:39 2000 +0200
@@ -17,25 +17,28 @@
 instance "*" :: (finite,finite) finite   (finite_Prod)
 
 
-consts
-  less_than :: "(nat*nat)set"
-  inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
-  measure   :: "('a => nat) => ('a * 'a)set"
-  lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
-               (infixr "<*lex*>" 80)
-  finite_psubset  :: "('a set * 'a set) set"
+constdefs
+ less_than :: "(nat*nat)set"
+"less_than == trancl pred_nat"
 
+ inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
+"inv_image r f == {(x,y). (f(x), f(y)) : r}"
+
+ measure   :: "('a => nat) => ('a * 'a)set"
+"measure == inv_image less_than"
 
-defs
-  less_than_def "less_than == trancl pred_nat"
+ lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
+               (infixr "<*lex*>" 80)
+"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
 
-  inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}"
-
-  measure_def   "measure == inv_image less_than"
+ (* finite proper subset*)
+ finite_psubset  :: "('a set * 'a set) set"
+"finite_psubset == {(A,B). A < B & finite B}"
 
-  lex_prod_def  "ra <*lex*> rb == {((a,b),(a',b')) | a a' b b'.
-                                   ((a,a') : ra | a=a' & (b,b') : rb)}"
+(* For rec_defs where the first n parameters stay unchanged in the recursive
+   call. See While for an application.
+*)
+ same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
+"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
 
-  (* finite proper subset*)
-  finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}"
 end