Measure functions can now be declared via special rules, allowing for a
authorkrauss
Mon May 12 22:11:06 2008 +0200 (2008-05-12)
changeset 26875e18574413bc4
parent 26874 b2daa27fc0a7
child 26876 d50ef6b952ba
Measure functions can now be declared via special rules, allowing for a
prolog-style generation of measure functions for a specific type.
src/HOL/FunDef.thy
src/HOL/List.thy
src/HOL/SizeChange/Examples.thy
src/HOL/SizeChange/sct.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Tools/function_package/measure_functions.ML
     1.1 --- a/src/HOL/FunDef.thy	Mon May 12 22:03:33 2008 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Mon May 12 22:11:06 2008 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4    ("Tools/function_package/fundef_package.ML")
     1.5    ("Tools/function_package/auto_term.ML")
     1.6    ("Tools/function_package/induction_scheme.ML")
     1.7 +  ("Tools/function_package/measure_functions.ML")
     1.8    ("Tools/function_package/lexicographic_order.ML")
     1.9    ("Tools/function_package/fundef_datatype.ML")
    1.10  begin
    1.11 @@ -96,6 +97,8 @@
    1.12    "wf R \<Longrightarrow> wfP (in_rel R)"
    1.13    by (simp add: wfP_def)
    1.14  
    1.15 +inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
    1.16 +where is_measure_trivial: "is_measure f"
    1.17  
    1.18  use "Tools/function_package/fundef_lib.ML"
    1.19  use "Tools/function_package/fundef_common.ML"
    1.20 @@ -108,12 +111,14 @@
    1.21  use "Tools/function_package/auto_term.ML"
    1.22  use "Tools/function_package/fundef_package.ML"
    1.23  use "Tools/function_package/induction_scheme.ML"
    1.24 +use "Tools/function_package/measure_functions.ML"
    1.25  use "Tools/function_package/lexicographic_order.ML"
    1.26  use "Tools/function_package/fundef_datatype.ML"
    1.27  
    1.28  setup {* 
    1.29    FundefPackage.setup 
    1.30    #> InductionScheme.setup
    1.31 +  #> MeasureFunctions.setup
    1.32    #> LexicographicOrder.setup 
    1.33    #> FundefDatatype.setup
    1.34  *}
    1.35 @@ -135,10 +140,31 @@
    1.36    "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
    1.37    unfolding o_apply .
    1.38  
    1.39 +subsection {* Setup for termination proofs *}
    1.40 +
    1.41 +text {* Rules for generating measure functions *}
    1.42 +
    1.43 +lemma [measure_function]: "is_measure size"
    1.44 +by (rule is_measure_trivial)
    1.45 +
    1.46 +lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
    1.47 +by (rule is_measure_trivial)
    1.48 +lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
    1.49 +by (rule is_measure_trivial)
    1.50 +
    1.51  lemma termination_basic_simps[termination_simp]:
    1.52 -  "x < y \<Longrightarrow> x < Suc y"
    1.53    "x < (y::nat) \<Longrightarrow> x < y + z" 
    1.54    "x < z \<Longrightarrow> x < y + z"
    1.55 +  "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
    1.56 +  "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
    1.57 +  "x < y \<Longrightarrow> x \<le> (y::nat)"
    1.58  by arith+
    1.59  
    1.60 +declare le_imp_less_Suc[termination_simp]
    1.61 +
    1.62 +lemma prod_size_simp[termination_simp]:
    1.63 +  "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
    1.64 +by (induct p) auto
    1.65 +
    1.66 +
    1.67  end
     2.1 --- a/src/HOL/List.thy	Mon May 12 22:03:33 2008 +0200
     2.2 +++ b/src/HOL/List.thy	Mon May 12 22:11:06 2008 +0200
     2.3 @@ -3313,12 +3313,26 @@
     2.4  
     2.5  subsection {* Size function *}
     2.6  
     2.7 -declare [[measure_function "list_size size"]]
     2.8 -
     2.9 -lemma list_size_estimation[termination_simp]:
    2.10 -  "x \<in> set xs \<Longrightarrow> f x < list_size f xs"
    2.11 +lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
    2.12 +by (rule is_measure_trivial)
    2.13 +
    2.14 +lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
    2.15 +by (rule is_measure_trivial)
    2.16 +
    2.17 +lemma list_size_estimation[termination_simp]: 
    2.18 +  "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
    2.19  by (induct xs) auto
    2.20  
    2.21 +lemma list_size_estimation'[termination_simp]: 
    2.22 +  "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
    2.23 +by (induct xs) auto
    2.24 +
    2.25 +lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
    2.26 +by (induct xs) auto
    2.27 +
    2.28 +lemma list_size_pointwise[termination_simp]: 
    2.29 +  "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
    2.30 +by (induct xs) force+
    2.31  
    2.32  subsection {* Code generator *}
    2.33  
     3.1 --- a/src/HOL/SizeChange/Examples.thy	Mon May 12 22:03:33 2008 +0200
     3.2 +++ b/src/HOL/SizeChange/Examples.thy	Mon May 12 22:11:06 2008 +0200
     3.3 @@ -22,7 +22,7 @@
     3.4    apply (rule SCT_on_relations)
     3.5    apply (tactic "Sct.abs_rel_tac") (* Build call descriptors *)
     3.6    apply (rule ext, rule ext, simp) (* Show that they are correct *)
     3.7 -  apply (tactic "Sct.mk_call_graph") (* Build control graph *)
     3.8 +  apply (tactic "Sct.mk_call_graph @{context}") (* Build control graph *)
     3.9    apply (rule SCT_Main)                 (* Apply main theorem *)
    3.10    apply (simp add:finite_acg_simps) (* show finiteness *)
    3.11    oops (*FIXME by eval*) (* Evaluate to true *)
    3.12 @@ -39,7 +39,7 @@
    3.13    apply (rule SCT_on_relations)
    3.14    apply (tactic "Sct.abs_rel_tac") 
    3.15    apply (rule ext, rule ext, simp) 
    3.16 -  apply (tactic "Sct.mk_call_graph")
    3.17 +  apply (tactic "Sct.mk_call_graph @{context}")
    3.18    apply (rule SCT_Main)
    3.19    apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
    3.20    oops (* FIXME by eval *)
    3.21 @@ -57,7 +57,7 @@
    3.22    apply (rule SCT_on_relations)
    3.23    apply (tactic "Sct.abs_rel_tac") 
    3.24    apply (rule ext, rule ext, simp) 
    3.25 -  apply (tactic "Sct.mk_call_graph")
    3.26 +  apply (tactic "Sct.mk_call_graph @{context}")
    3.27    apply (rule SCT_Main)
    3.28    apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
    3.29    oops (* FIXME by eval *)
    3.30 @@ -75,7 +75,7 @@
    3.31    apply (rule SCT_on_relations)
    3.32    apply (tactic "Sct.abs_rel_tac") 
    3.33    apply (rule ext, rule ext, simp) 
    3.34 -  apply (tactic "Sct.mk_call_graph")
    3.35 +  apply (tactic "Sct.mk_call_graph @{context}")
    3.36    apply (rule SCT_Main)
    3.37    apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
    3.38    by (simp only:sctTest_simps cong: sctTest_congs)
     4.1 --- a/src/HOL/SizeChange/sct.ML	Mon May 12 22:03:33 2008 +0200
     4.2 +++ b/src/HOL/SizeChange/sct.ML	Mon May 12 22:11:06 2008 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  signature SCT =
     4.5  sig
     4.6    val abs_rel_tac : tactic
     4.7 -  val mk_call_graph : tactic
     4.8 +  val mk_call_graph : Proof.context -> tactic
     4.9  end
    4.10  
    4.11  structure Sct : SCT =
    4.12 @@ -146,10 +146,10 @@
    4.13  
    4.14  
    4.15  (* very primitive *)
    4.16 -fun measures_of thy RD =
    4.17 +fun measures_of ctxt RD =
    4.18      let
    4.19        val domT = range_type (fastype_of (fst (HOLogic.dest_prod (snd (HOLogic.dest_prod RD)))))
    4.20 -      val measures = LexicographicOrder.mk_base_funs thy domT
    4.21 +      val measures = MeasureFunctions.get_measure_functions ctxt domT
    4.22      in
    4.23        measures
    4.24      end
    4.25 @@ -300,7 +300,7 @@
    4.26  
    4.27  
    4.28  
    4.29 -fun mk_call_graph (st : thm) =
    4.30 +fun mk_call_graph ctxt (st : thm) =
    4.31      let
    4.32        val thy = theory_of_thm st
    4.33        val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st))
    4.34 @@ -308,7 +308,7 @@
    4.35        val RDs = HOLogic.dest_list RDlist
    4.36        val n = length RDs
    4.37  
    4.38 -      val Mss = map (measures_of thy) RDs
    4.39 +      val Mss = map (measures_of ctxt) RDs
    4.40  
    4.41        val domT = domain_type (fastype_of (hd (hd Mss)))
    4.42  
     5.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Mon May 12 22:03:33 2008 +0200
     5.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Mon May 12 22:11:06 2008 +0200
     5.3 @@ -9,9 +9,6 @@
     5.4  sig
     5.5    val lexicographic_order : thm list -> Proof.context -> Method.method
     5.6  
     5.7 -  (* exported for use by size-change termination prototype.
     5.8 -     FIXME: provide a common interface later *)
     5.9 -  val mk_base_funs : theory -> typ -> term list
    5.10    (* exported for debugging *)
    5.11    val setup: theory -> theory
    5.12  end
    5.13 @@ -19,29 +16,6 @@
    5.14  structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
    5.15  struct
    5.16  
    5.17 -(** User-declared size functions **)
    5.18 -
    5.19 -structure SizeFunsData = GenericDataFun
    5.20 -(
    5.21 -  type T = term NetRules.T;
    5.22 -  val empty = NetRules.init (op aconv) I
    5.23 -  val copy = I
    5.24 -  val extend = I
    5.25 -  fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
    5.26 -);
    5.27 -
    5.28 -fun add_sfun f ctxt = 
    5.29 -  SizeFunsData.map (NetRules.insert (singleton (Variable.polymorphic (Context.proof_of ctxt)) f)) ctxt
    5.30 -val add_sfun_attr = Attrib.syntax (Args.term >> (fn f => Thm.declaration_attribute (K (add_sfun f))))
    5.31 -
    5.32 -fun get_sfuns T thy =
    5.33 -    map_filter (fn f => SOME (Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy)
    5.34 -                                                                (domain_type (fastype_of f), T)
    5.35 -                                                                Vartab.empty) 
    5.36 -                                                f)
    5.37 -                   handle Type.TYPE_MATCH => NONE)
    5.38 -               (NetRules.rules (SizeFunsData.get (Context.Theory thy)))
    5.39 -
    5.40  (** General stuff **)
    5.41  
    5.42  fun mk_measures domT mfuns =
    5.43 @@ -72,62 +46,12 @@
    5.44  fun is_LessEq (LessEq _) = true
    5.45    | is_LessEq _ = false
    5.46  
    5.47 -fun thm_of_cell (Less thm) = thm
    5.48 -  | thm_of_cell (LessEq (thm, _)) = thm
    5.49 -  | thm_of_cell (False thm) = thm
    5.50 -  | thm_of_cell (None (thm, _)) = thm
    5.51 -
    5.52  fun pr_cell (Less _ ) = " < "
    5.53    | pr_cell (LessEq _) = " <="
    5.54    | pr_cell (None _) = " ? "
    5.55    | pr_cell (False _) = " F "
    5.56  
    5.57  
    5.58 -(** Generating Measure Functions **)
    5.59 -
    5.60 -fun mk_comp g f =
    5.61 -    let
    5.62 -      val fT = fastype_of f
    5.63 -      val gT as (Type ("fun", [xT, _])) = fastype_of g
    5.64 -      val comp = Abs ("f", fT, Abs ("g", gT, Abs ("x", xT, Bound 2 $ (Bound 1 $ Bound 0))))
    5.65 -    in
    5.66 -      Envir.beta_norm (comp $ f $ g)
    5.67 -    end
    5.68 -
    5.69 -fun mk_base_funs thy (T as Type("*", [fT, sT])) = (* products *)
    5.70 -      map (mk_comp (Const ("fst", T --> fT))) (mk_base_funs thy fT)
    5.71 -    @ map (mk_comp (Const ("snd", T --> sT))) (mk_base_funs thy sT)
    5.72 -
    5.73 -  | mk_base_funs thy T = (* default: size function, if available *)
    5.74 -    if Sorts.of_sort (Sign.classes_of thy) (T, [HOLogic.class_size])
    5.75 -    then (HOLogic.size_const T) :: get_sfuns T thy
    5.76 -    else get_sfuns T thy
    5.77 -
    5.78 -fun mk_sum_case f1 f2 =
    5.79 -    let
    5.80 -      val Type ("fun", [fT, Q]) = fastype_of f1
    5.81 -      val Type ("fun", [sT, _]) = fastype_of f2
    5.82 -    in
    5.83 -      Const (@{const_name "Sum_Type.sum_case"}, (fT --> Q) --> (sT --> Q) --> Type("+", [fT, sT]) --> Q) $ f1 $ f2
    5.84 -    end
    5.85 -
    5.86 -fun constant_0 T = Abs ("x", T, HOLogic.zero)
    5.87 -fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
    5.88 -
    5.89 -fun mk_funorder_funs (Type ("+", [fT, sT])) =
    5.90 -      map (fn m => mk_sum_case m (constant_0 sT)) (mk_funorder_funs fT)
    5.91 -    @ map (fn m => mk_sum_case (constant_0 fT) m) (mk_funorder_funs sT)
    5.92 -  | mk_funorder_funs T = [ constant_1 T ]
    5.93 -
    5.94 -fun mk_ext_base_funs thy (Type("+", [fT, sT])) =
    5.95 -      map_product mk_sum_case (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT)
    5.96 -  | mk_ext_base_funs thy T = mk_base_funs thy T
    5.97 -
    5.98 -fun mk_all_measure_funs thy (T as Type ("+", _)) =
    5.99 -    mk_ext_base_funs thy T @ mk_funorder_funs T
   5.100 -  | mk_all_measure_funs thy T = mk_base_funs thy T
   5.101 -
   5.102 -
   5.103  (** Proof attempts to build the matrix **)
   5.104  
   5.105  fun dest_term (t : term) =
   5.106 @@ -260,7 +184,7 @@
   5.107  fun pr_unprovable_cell _ ((i,j), Less _) = ""
   5.108    | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
   5.109        "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
   5.110 -  | pr_unprovable_cell ctxt ((i,j), None (st_less, st_leq)) =
   5.111 +  | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
   5.112        "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less
   5.113        ^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq
   5.114    | pr_unprovable_cell ctxt ((i,j), False st) =
   5.115 @@ -303,7 +227,7 @@
   5.116  
   5.117        val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
   5.118  
   5.119 -      val measure_funs = mk_all_measure_funs thy domT (* 1: generate measures *)
   5.120 +      val measure_funs = MeasureFunctions.get_measure_functions ctxt domT (* 1: generate measures *)
   5.121  
   5.122        (* 2: create table *)
   5.123        val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
   5.124 @@ -329,6 +253,5 @@
   5.125  
   5.126  val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
   5.127                                   "termination prover for lexicographic orderings")]
   5.128 -    #> Attrib.add_attributes [("measure_function", add_sfun_attr, "declare custom measure function")]
   5.129  
   5.130  end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/function_package/measure_functions.ML	Mon May 12 22:11:06 2008 +0200
     6.3 @@ -0,0 +1,59 @@
     6.4 +(*  Title:       HOL/Tools/function_package/measure_functions.ML
     6.5 +    ID:          $Id$
     6.6 +    Author:      Alexander Krauss, TU Muenchen
     6.7 +
     6.8 +Measure functions, generated heuristically
     6.9 +*)
    6.10 +
    6.11 +signature MEASURE_FUNCTIONS =
    6.12 +sig
    6.13 +
    6.14 +  val get_measure_functions : Proof.context -> typ -> term list
    6.15 +  val setup : theory -> theory                                                      
    6.16 +
    6.17 +end
    6.18 +
    6.19 +structure MeasureFunctions : MEASURE_FUNCTIONS = 
    6.20 +struct 
    6.21 +
    6.22 +(** User-declared size functions **)
    6.23 +structure MeasureHeuristicRules = NamedThmsFun(
    6.24 +  val name = "measure_function" 
    6.25 +  val description = "Rules that guide the heuristic generation of measure functions"
    6.26 +);
    6.27 +
    6.28 +fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
    6.29 +
    6.30 +fun find_measures ctxt T =
    6.31 +  DEPTH_SOLVE (resolve_tac (MeasureHeuristicRules.get ctxt) 1) 
    6.32 +    (HOLogic.mk_Trueprop (mk_is_measures (Var (("f",0), T --> HOLogic.natT)))
    6.33 +      |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init)
    6.34 +  |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f))
    6.35 +  |> Seq.list_of
    6.36 +
    6.37 +
    6.38 +(** Generating Measure Functions **)
    6.39 +
    6.40 +fun constant_0 T = Abs ("x", T, HOLogic.zero)
    6.41 +fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
    6.42 +
    6.43 +fun mk_funorder_funs (Type ("+", [fT, sT])) =
    6.44 +      map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
    6.45 +    @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
    6.46 +  | mk_funorder_funs T = [ constant_1 T ]
    6.47 +
    6.48 +fun mk_ext_base_funs ctxt (Type("+", [fT, sT])) =
    6.49 +      map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
    6.50 +                  (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
    6.51 +  | mk_ext_base_funs ctxt T = find_measures ctxt T
    6.52 +
    6.53 +fun mk_all_measure_funs ctxt (T as Type ("+", _)) =
    6.54 +    mk_ext_base_funs ctxt T @ mk_funorder_funs T
    6.55 +  | mk_all_measure_funs ctxt T = find_measures ctxt T
    6.56 +
    6.57 +val get_measure_functions = mk_all_measure_funs
    6.58 +
    6.59 +val setup = MeasureHeuristicRules.setup
    6.60 +
    6.61 +end
    6.62 +