Measure functions can now be declared via special rules, allowing for a
prolog-style generation of measure functions for a specific type.

--- a/src/HOL/FunDef.thy	Mon May 12 22:03:33 2008 +0200
+++ b/src/HOL/FunDef.thy	Mon May 12 22:11:06 2008 +0200
@@ -19,6 +19,7 @@
   ("Tools/function_package/fundef_package.ML")
   ("Tools/function_package/auto_term.ML")
   ("Tools/function_package/induction_scheme.ML")
+  ("Tools/function_package/measure_functions.ML")
   ("Tools/function_package/lexicographic_order.ML")
   ("Tools/function_package/fundef_datatype.ML")
 begin
@@ -96,6 +97,8 @@
   "wf R \<Longrightarrow> wfP (in_rel R)"
   by (simp add: wfP_def)
 
+inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
+where is_measure_trivial: "is_measure f"
 
 use "Tools/function_package/fundef_lib.ML"
 use "Tools/function_package/fundef_common.ML"
@@ -108,12 +111,14 @@
 use "Tools/function_package/auto_term.ML"
 use "Tools/function_package/fundef_package.ML"
 use "Tools/function_package/induction_scheme.ML"
+use "Tools/function_package/measure_functions.ML"
 use "Tools/function_package/lexicographic_order.ML"
 use "Tools/function_package/fundef_datatype.ML"
 
 setup {* 
   FundefPackage.setup 
   #> InductionScheme.setup
+  #> MeasureFunctions.setup
   #> LexicographicOrder.setup 
   #> FundefDatatype.setup
 *}
@@ -135,10 +140,31 @@
   "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
   unfolding o_apply .
 
+subsection {* Setup for termination proofs *}
+
+text {* Rules for generating measure functions *}
+
+lemma [measure_function]: "is_measure size"
+by (rule is_measure_trivial)
+
+lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
+by (rule is_measure_trivial)
+lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
+by (rule is_measure_trivial)
+
 lemma termination_basic_simps[termination_simp]:
-  "x < y \<Longrightarrow> x < Suc y"
   "x < (y::nat) \<Longrightarrow> x < y + z" 
   "x < z \<Longrightarrow> x < y + z"
+  "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
+  "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
+  "x < y \<Longrightarrow> x \<le> (y::nat)"
 by arith+
 
+declare le_imp_less_Suc[termination_simp]
+
+lemma prod_size_simp[termination_simp]:
+  "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
+by (induct p) auto
+
+
 end

--- a/src/HOL/List.thy	Mon May 12 22:03:33 2008 +0200
+++ b/src/HOL/List.thy	Mon May 12 22:11:06 2008 +0200
@@ -3313,12 +3313,26 @@
 
 subsection {* Size function *}
 
-declare [[measure_function "list_size size"]]
-
-lemma list_size_estimation[termination_simp]:
-  "x \<in> set xs \<Longrightarrow> f x < list_size f xs"
+lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
+by (rule is_measure_trivial)
+
+lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
+by (rule is_measure_trivial)
+
+lemma list_size_estimation[termination_simp]: 
+  "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
 by (induct xs) auto
 
+lemma list_size_estimation'[termination_simp]: 
+  "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
+by (induct xs) auto
+
+lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
+by (induct xs) auto
+
+lemma list_size_pointwise[termination_simp]: 
+  "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
+by (induct xs) force+
 
 subsection {* Code generator *}
 

--- a/src/HOL/SizeChange/Examples.thy	Mon May 12 22:03:33 2008 +0200
+++ b/src/HOL/SizeChange/Examples.thy	Mon May 12 22:11:06 2008 +0200
@@ -22,7 +22,7 @@
   apply (rule SCT_on_relations)
   apply (tactic "Sct.abs_rel_tac") (* Build call descriptors *)
   apply (rule ext, rule ext, simp) (* Show that they are correct *)
-  apply (tactic "Sct.mk_call_graph") (* Build control graph *)
+  apply (tactic "Sct.mk_call_graph @{context}") (* Build control graph *)
   apply (rule SCT_Main)                 (* Apply main theorem *)
   apply (simp add:finite_acg_simps) (* show finiteness *)
   oops (*FIXME by eval*) (* Evaluate to true *)
@@ -39,7 +39,7 @@
   apply (rule SCT_on_relations)
   apply (tactic "Sct.abs_rel_tac") 
   apply (rule ext, rule ext, simp) 
-  apply (tactic "Sct.mk_call_graph")
+  apply (tactic "Sct.mk_call_graph @{context}")
   apply (rule SCT_Main)
   apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
   oops (* FIXME by eval *)
@@ -57,7 +57,7 @@
   apply (rule SCT_on_relations)
   apply (tactic "Sct.abs_rel_tac") 
   apply (rule ext, rule ext, simp) 
-  apply (tactic "Sct.mk_call_graph")
+  apply (tactic "Sct.mk_call_graph @{context}")
   apply (rule SCT_Main)
   apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
   oops (* FIXME by eval *)
@@ -75,7 +75,7 @@
   apply (rule SCT_on_relations)
   apply (tactic "Sct.abs_rel_tac") 
   apply (rule ext, rule ext, simp) 
-  apply (tactic "Sct.mk_call_graph")
+  apply (tactic "Sct.mk_call_graph @{context}")
   apply (rule SCT_Main)
   apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
   by (simp only:sctTest_simps cong: sctTest_congs)

--- a/src/HOL/SizeChange/sct.ML	Mon May 12 22:03:33 2008 +0200
+++ b/src/HOL/SizeChange/sct.ML	Mon May 12 22:11:06 2008 +0200
@@ -7,7 +7,7 @@
 signature SCT =
 sig
   val abs_rel_tac : tactic
-  val mk_call_graph : tactic
+  val mk_call_graph : Proof.context -> tactic
 end
 
 structure Sct : SCT =
@@ -146,10 +146,10 @@
 
 
 (* very primitive *)
-fun measures_of thy RD =
+fun measures_of ctxt RD =
     let
       val domT = range_type (fastype_of (fst (HOLogic.dest_prod (snd (HOLogic.dest_prod RD)))))
-      val measures = LexicographicOrder.mk_base_funs thy domT
+      val measures = MeasureFunctions.get_measure_functions ctxt domT
     in
       measures
     end
@@ -300,7 +300,7 @@
 
 
 
-fun mk_call_graph (st : thm) =
+fun mk_call_graph ctxt (st : thm) =
     let
       val thy = theory_of_thm st
       val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st))
@@ -308,7 +308,7 @@
       val RDs = HOLogic.dest_list RDlist
       val n = length RDs
 
-      val Mss = map (measures_of thy) RDs
+      val Mss = map (measures_of ctxt) RDs
 
       val domT = domain_type (fastype_of (hd (hd Mss)))
 

--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Mon May 12 22:03:33 2008 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Mon May 12 22:11:06 2008 +0200
@@ -9,9 +9,6 @@
 sig
   val lexicographic_order : thm list -> Proof.context -> Method.method
 
-  (* exported for use by size-change termination prototype.
-     FIXME: provide a common interface later *)
-  val mk_base_funs : theory -> typ -> term list
   (* exported for debugging *)
   val setup: theory -> theory
 end
@@ -19,29 +16,6 @@
 structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
 struct
 
-(** User-declared size functions **)
-
-structure SizeFunsData = GenericDataFun
-(
-  type T = term NetRules.T;
-  val empty = NetRules.init (op aconv) I
-  val copy = I
-  val extend = I
-  fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
-);
-
-fun add_sfun f ctxt = 
-  SizeFunsData.map (NetRules.insert (singleton (Variable.polymorphic (Context.proof_of ctxt)) f)) ctxt
-val add_sfun_attr = Attrib.syntax (Args.term >> (fn f => Thm.declaration_attribute (K (add_sfun f))))
-
-fun get_sfuns T thy =
-    map_filter (fn f => SOME (Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy)
-                                                                (domain_type (fastype_of f), T)
-                                                                Vartab.empty) 
-                                                f)
-                   handle Type.TYPE_MATCH => NONE)
-               (NetRules.rules (SizeFunsData.get (Context.Theory thy)))
-
 (** General stuff **)
 
 fun mk_measures domT mfuns =
@@ -72,62 +46,12 @@
 fun is_LessEq (LessEq _) = true
   | is_LessEq _ = false
 
-fun thm_of_cell (Less thm) = thm
-  | thm_of_cell (LessEq (thm, _)) = thm
-  | thm_of_cell (False thm) = thm
-  | thm_of_cell (None (thm, _)) = thm
-
 fun pr_cell (Less _ ) = " < "
   | pr_cell (LessEq _) = " <="
   | pr_cell (None _) = " ? "
   | pr_cell (False _) = " F "
 
 
-(** Generating Measure Functions **)
-
-fun mk_comp g f =
-    let
-      val fT = fastype_of f
-      val gT as (Type ("fun", [xT, _])) = fastype_of g
-      val comp = Abs ("f", fT, Abs ("g", gT, Abs ("x", xT, Bound 2 $ (Bound 1 $ Bound 0))))
-    in
-      Envir.beta_norm (comp $ f $ g)
-    end
-
-fun mk_base_funs thy (T as Type("*", [fT, sT])) = (* products *)
-      map (mk_comp (Const ("fst", T --> fT))) (mk_base_funs thy fT)
-    @ map (mk_comp (Const ("snd", T --> sT))) (mk_base_funs thy sT)
-
-  | mk_base_funs thy T = (* default: size function, if available *)
-    if Sorts.of_sort (Sign.classes_of thy) (T, [HOLogic.class_size])
-    then (HOLogic.size_const T) :: get_sfuns T thy
-    else get_sfuns T thy
-
-fun mk_sum_case f1 f2 =
-    let
-      val Type ("fun", [fT, Q]) = fastype_of f1
-      val Type ("fun", [sT, _]) = fastype_of f2
-    in
-      Const (@{const_name "Sum_Type.sum_case"}, (fT --> Q) --> (sT --> Q) --> Type("+", [fT, sT]) --> Q) $ f1 $ f2
-    end
-
-fun constant_0 T = Abs ("x", T, HOLogic.zero)
-fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
-
-fun mk_funorder_funs (Type ("+", [fT, sT])) =
-      map (fn m => mk_sum_case m (constant_0 sT)) (mk_funorder_funs fT)
-    @ map (fn m => mk_sum_case (constant_0 fT) m) (mk_funorder_funs sT)
-  | mk_funorder_funs T = [ constant_1 T ]
-
-fun mk_ext_base_funs thy (Type("+", [fT, sT])) =
-      map_product mk_sum_case (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT)
-  | mk_ext_base_funs thy T = mk_base_funs thy T
-
-fun mk_all_measure_funs thy (T as Type ("+", _)) =
-    mk_ext_base_funs thy T @ mk_funorder_funs T
-  | mk_all_measure_funs thy T = mk_base_funs thy T
-
-
 (** Proof attempts to build the matrix **)
 
 fun dest_term (t : term) =
@@ -260,7 +184,7 @@
 fun pr_unprovable_cell _ ((i,j), Less _) = ""
   | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
       "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
-  | pr_unprovable_cell ctxt ((i,j), None (st_less, st_leq)) =
+  | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
       "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less
       ^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq
   | pr_unprovable_cell ctxt ((i,j), False st) =
@@ -303,7 +227,7 @@
 
       val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
 
-      val measure_funs = mk_all_measure_funs thy domT (* 1: generate measures *)
+      val measure_funs = MeasureFunctions.get_measure_functions ctxt domT (* 1: generate measures *)
 
       (* 2: create table *)
       val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
@@ -329,6 +253,5 @@
 
 val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
                                  "termination prover for lexicographic orderings")]
-    #> Attrib.add_attributes [("measure_function", add_sfun_attr, "declare custom measure function")]
 
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/measure_functions.ML	Mon May 12 22:11:06 2008 +0200
@@ -0,0 +1,59 @@
+(*  Title:       HOL/Tools/function_package/measure_functions.ML
+    ID:          $Id$
+    Author:      Alexander Krauss, TU Muenchen
+
+Measure functions, generated heuristically
+*)
+
+signature MEASURE_FUNCTIONS =
+sig
+
+  val get_measure_functions : Proof.context -> typ -> term list
+  val setup : theory -> theory                                                      
+
+end
+
+structure MeasureFunctions : MEASURE_FUNCTIONS = 
+struct 
+
+(** User-declared size functions **)
+structure MeasureHeuristicRules = NamedThmsFun(
+  val name = "measure_function" 
+  val description = "Rules that guide the heuristic generation of measure functions"
+);
+
+fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
+
+fun find_measures ctxt T =
+  DEPTH_SOLVE (resolve_tac (MeasureHeuristicRules.get ctxt) 1) 
+    (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT)))
+      |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
+  |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
+  |> Seq.list_of
+
+
+(** Generating Measure Functions **)
+
+fun constant_0 T = Abs ("x", T, HOLogic.zero)
+fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
+
+fun mk_funorder_funs (Type ("+", [fT, sT])) =
+      map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
+    @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
+  | mk_funorder_funs T = [ constant_1 T ]
+
+fun mk_ext_base_funs ctxt (Type("+", [fT, sT])) =
+      map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
+                  (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
+  | mk_ext_base_funs ctxt T = find_measures ctxt T
+
+fun mk_all_measure_funs ctxt (T as Type ("+", _)) =
+    mk_ext_base_funs ctxt T @ mk_funorder_funs T
+  | mk_all_measure_funs ctxt T = find_measures ctxt T
+
+val get_measure_functions = mk_all_measure_funs
+
+val setup = MeasureHeuristicRules.setup
+
+end
+