# HG changeset patch
# User krauss
# Date 1189801373 -7200
# Node ID 32ddd902b0adbb6dc5b6669c46095f186dbcfc1b
# Parent  8b5c5eb7df876de85beeff5b98a1fa43ee7b1c56
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy

diff -r 8b5c5eb7df87 -r 32ddd902b0ad src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Sep 14 22:21:46 2007 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Sep 14 22:22:53 2007 +0200
@@ -22,9 +22,14 @@
 (** General stuff **)
 
 fun mk_measures domT mfuns =
-    let val list = HOLogic.mk_list (domT --> HOLogic.natT) mfuns
+    let 
+        val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
+        val mlexT = (domT --> HOLogic.natT) --> relT --> relT
+        fun mk_ms [] = Const (@{const_name "{}"}, relT)
+          | mk_ms (f::fs) = 
+            Const (@{const_name "Wellfounded_Relations.mlex_prod"}, mlexT) $ f $ mk_ms fs
     in
-      Const (@{const_name "List.measures"}, fastype_of list --> (HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))) $ list
+        mk_ms mfuns
     end
 
 fun del_index n [] = []
@@ -36,7 +41,7 @@
 
 (** Matrix cell datatype **)
 
-datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
+datatype cell = Less of thm| LessEq of (thm * thm) | None of (thm * thm) | False of thm;
 
 fun is_Less (Less _) = true
   | is_Less _ = false
@@ -209,10 +214,10 @@
 
 (* prove row :: cell list -> tactic *)
 fun prove_row (Less less_thm :: _) =
-    (rtac @{thm "measures_less"} 1)
+    (rtac @{thm "mlex_less"} 1)
     THEN PRIMITIVE (flip implies_elim less_thm)
   | prove_row (LessEq (lesseq_thm, _) :: tail) =
-    (rtac @{thm "measures_lesseq"} 1)
+    (rtac @{thm "mlex_leq"} 1)
     THEN PRIMITIVE (flip implies_elim lesseq_thm)
     THEN prove_row tail
   | prove_row _ = sys_error "lexicographic_order"
@@ -291,7 +296,8 @@
 
     in (* 4: proof reconstruction *)
       st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
-              THEN rtac @{thm "wf_measures"} 1
+              THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
+              THEN (rtac @{thm "wf_empty"} 1)
               THEN EVERY (map prove_row clean_table))
     end