# HG changeset patch
# User paulson
# Date 864121228 -7200
# Node ID 4da86d44de33f9e29cc8178e84f6b7299f55530f
# Parent  882e125ed7da9e10417e2863fdde658e617acf9c
Relation "less_than" internalizes "<" for easy use of TFL

diff -r 882e125ed7da -r 4da86d44de33 src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Tue May 20 11:39:32 1997 +0200
+++ b/src/HOL/WF_Rel.ML	Tue May 20 11:40:28 1997 +0200
@@ -10,6 +10,25 @@
 
 
 (*----------------------------------------------------------------------------
+ * "Less than" on the natural numbers
+ *---------------------------------------------------------------------------*)
+
+goalw thy [less_than_def] "wf less_than"; 
+by (rtac (wf_pred_nat RS wf_trancl) 1);
+qed "wf_less_than";
+AddIffs [wf_less_than];
+
+goalw thy [less_than_def] "trans less_than"; 
+by (rtac trans_trancl 1);
+qed "trans_less_than";
+AddIffs [trans_less_than];
+
+goalw thy [less_than_def, less_def] "((x,y): less_than) = (x<y)"; 
+by (Simp_tac 1);
+qed "less_than_iff";
+AddIffs [less_than_iff];
+
+(*----------------------------------------------------------------------------
  * The inverse image into a wellfounded relation is wellfounded.
  *---------------------------------------------------------------------------*)
 
@@ -24,14 +43,19 @@
 qed "wf_inv_image";
 AddSIs [wf_inv_image];
 
+goalw thy [trans_def,inv_image_def]
+    "!!r. trans r ==> trans (inv_image r f)";
+by (Simp_tac 1);
+by (Blast_tac 1);
+qed "trans_inv_image";
+
+
 (*----------------------------------------------------------------------------
  * All measures are wellfounded.
  *---------------------------------------------------------------------------*)
 
 goalw thy [measure_def] "wf (measure f)";
-by (rtac wf_inv_image 1);
-by (rtac wf_trancl 1);
-by (rtac wf_pred_nat 1);
+by (rtac (wf_less_than RS wf_inv_image) 1);
 qed "wf_measure";
 AddIffs [wf_measure];
 
@@ -111,9 +135,13 @@
  *---------------------------------------------------------------------------*)
 goalw thy [finite_psubset_def] "wf(finite_psubset)";
 by (rtac (wf_measure RS wf_subset) 1);
-by (simp_tac (!simpset addsimps[measure_def, inv_image_def,
-				symmetric less_def])1);
+by (simp_tac (!simpset addsimps [measure_def, inv_image_def, less_than_def,
+				 symmetric less_def])1);
 by (fast_tac (!claset addIs [psubset_card]) 1);
 qed "wf_finite_psubset";
 
+goalw thy [finite_psubset_def, trans_def] "trans finite_psubset";
+by (simp_tac (!simpset addsimps [psubset_def]) 1);
+by (Blast_tac 1);
+qed "trans_finite_psubset";
 
diff -r 882e125ed7da -r 4da86d44de33 src/HOL/WF_Rel.thy
--- a/src/HOL/WF_Rel.thy	Tue May 20 11:39:32 1997 +0200
+++ b/src/HOL/WF_Rel.thy	Tue May 20 11:40:28 1997 +0200
@@ -8,16 +8,20 @@
 
 WF_Rel = Finite +
 consts
- inv_image  :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
- measure    :: "('a => nat) => ('a * 'a)set"
-    "**"    :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
-   rprod    :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
-   finite_psubset  :: "('a set * 'a set) set"
+  less_than :: "(nat*nat)set"
+  inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
+  measure   :: "('a => nat) => ('a * 'a)set"
+  "**"      :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
+  rprod     :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
+  finite_psubset  :: "('a set * 'a set) set"
+
 
 defs
+  less_than_def "less_than == trancl pred_nat"
+
   inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}"
 
-  measure_def   "measure == inv_image (trancl pred_nat)"
+  measure_def   "measure == inv_image less_than"
 
   lex_prod_def  "ra**rb == {p. ? a a' b b'. 
                                 p = ((a,b),(a',b')) &