lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
authorkrauss
Fri Sep 14 22:22:53 2007 +0200 (2007-09-14)
changeset 2457632ddd902b0ad
parent 24575 8b5c5eb7df87
child 24577 c6acb6d79757
lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
src/HOL/Tools/function_package/lexicographic_order.ML
     1.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Sep 14 22:21:46 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Sep 14 22:22:53 2007 +0200
     1.3 @@ -22,9 +22,14 @@
     1.4  (** General stuff **)
     1.5  
     1.6  fun mk_measures domT mfuns =
     1.7 -    let val list = HOLogic.mk_list (domT --> HOLogic.natT) mfuns
     1.8 +    let 
     1.9 +        val relT = HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))
    1.10 +        val mlexT = (domT --> HOLogic.natT) --> relT --> relT
    1.11 +        fun mk_ms [] = Const (@{const_name "{}"}, relT)
    1.12 +          | mk_ms (f::fs) = 
    1.13 +            Const (@{const_name "Wellfounded_Relations.mlex_prod"}, mlexT) $ f $ mk_ms fs
    1.14      in
    1.15 -      Const (@{const_name "List.measures"}, fastype_of list --> (HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))) $ list
    1.16 +        mk_ms mfuns
    1.17      end
    1.18  
    1.19  fun del_index n [] = []
    1.20 @@ -36,7 +41,7 @@
    1.21  
    1.22  (** Matrix cell datatype **)
    1.23  
    1.24 -datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
    1.25 +datatype cell = Less of thm| LessEq of (thm * thm) | None of (thm * thm) | False of thm;
    1.26  
    1.27  fun is_Less (Less _) = true
    1.28    | is_Less _ = false
    1.29 @@ -209,10 +214,10 @@
    1.30  
    1.31  (* prove row :: cell list -> tactic *)
    1.32  fun prove_row (Less less_thm :: _) =
    1.33 -    (rtac @{thm "measures_less"} 1)
    1.34 +    (rtac @{thm "mlex_less"} 1)
    1.35      THEN PRIMITIVE (flip implies_elim less_thm)
    1.36    | prove_row (LessEq (lesseq_thm, _) :: tail) =
    1.37 -    (rtac @{thm "measures_lesseq"} 1)
    1.38 +    (rtac @{thm "mlex_leq"} 1)
    1.39      THEN PRIMITIVE (flip implies_elim lesseq_thm)
    1.40      THEN prove_row tail
    1.41    | prove_row _ = sys_error "lexicographic_order"
    1.42 @@ -291,7 +296,8 @@
    1.43  
    1.44      in (* 4: proof reconstruction *)
    1.45        st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
    1.46 -              THEN rtac @{thm "wf_measures"} 1
    1.47 +              THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
    1.48 +              THEN (rtac @{thm "wf_empty"} 1)
    1.49                THEN EVERY (map prove_row clean_table))
    1.50      end
    1.51