replaced "auto_term" by the simpler method "relation", which does not try
authorkrauss
Mon Nov 13 13:51:22 2006 +0100 (2006-11-13)
changeset 21319cf814e36f788
parent 21318 edb595802d22
child 21320 d240748a2cf5
replaced "auto_term" by the simpler method "relation", which does not try
to simplify. Some more cleanup.
src/HOL/FunDef.thy
src/HOL/Tools/function_package/auto_term.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Tools/function_package/mutual.ML
src/HOL/ex/CodeCollections.thy
src/HOL/ex/Codegenerator.thy
src/HOL/ex/Fundefs.thy
     1.1 --- a/src/HOL/FunDef.thy	Mon Nov 13 12:10:49 2006 +0100
     1.2 +++ b/src/HOL/FunDef.thy	Mon Nov 13 13:51:22 2006 +0100
     1.3 @@ -199,11 +199,10 @@
     1.4  use "Tools/function_package/termination.ML"
     1.5  use "Tools/function_package/mutual.ML"
     1.6  use "Tools/function_package/pattern_split.ML"
     1.7 +use "Tools/function_package/auto_term.ML"
     1.8  use "Tools/function_package/fundef_package.ML"
     1.9 -use "Tools/function_package/auto_term.ML"
    1.10  
    1.11  setup FundefPackage.setup
    1.12 -setup FundefAutoTerm.setup
    1.13  
    1.14  lemmas [fundef_cong] = 
    1.15    let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
     2.1 --- a/src/HOL/Tools/function_package/auto_term.ML	Mon Nov 13 12:10:49 2006 +0100
     2.2 +++ b/src/HOL/Tools/function_package/auto_term.ML	Mon Nov 13 13:51:22 2006 +0100
     2.3 @@ -3,48 +3,37 @@
     2.4      Author:     Alexander Krauss, TU Muenchen
     2.5  
     2.6  A package for general recursive function definitions.
     2.7 -The auto_term method.
     2.8 +Method "relation" to commence a termination proof using a user-specified relation.
     2.9  *)
    2.10  
    2.11  
    2.12 -signature FUNDEF_AUTO_TERM =
    2.13 +signature FUNDEF_RELATION =
    2.14  sig
    2.15 +  val relation_meth : Proof.context -> term -> Method.method
    2.16 +
    2.17    val setup: theory -> theory
    2.18  end
    2.19  
    2.20 -structure FundefAutoTerm : FUNDEF_AUTO_TERM =
    2.21 +structure FundefRelation : FUNDEF_RELATION =
    2.22  struct
    2.23  
    2.24 -open FundefCommon
    2.25 -open FundefAbbrev
    2.26 -
    2.27 -
    2.28 -fun auto_term_tac ctxt rule rel wf_rules ss =
    2.29 -  let
    2.30 -    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
    2.31 -
    2.32 -    val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
    2.33 -    val rule' = rule |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)
    2.34 -    val prem = #1 (Logic.dest_implies (Thm.prop_of rule'))
    2.35 -    val R' = cert (Var (the_single (Term.add_vars prem [])))
    2.36 -  in
    2.37 -    rtac (Drule.cterm_instantiate [(R', rel')] rule') 1  (* instantiate termination rule *)
    2.38 -    THEN (ALLGOALS
    2.39 -      (fn 1 => REPEAT (ares_tac wf_rules 1)    (* Solve wellfoundedness *)
    2.40 -        | i => asm_simp_tac ss i))             (* Simplify termination conditions *)
    2.41 -  end
    2.42 -
    2.43 -
    2.44 -fun termination_meth src = Method.syntax Args.term src #> (fn (ctxt, rel) =>
    2.45 -  let
    2.46 -    val {simps, congs, wfs} = RecdefPackage.get_hints (Context.Proof ctxt)
    2.47 -    val ss = local_simpset_of ctxt addsimps simps
    2.48 -
    2.49 -    val intro_rule = ProofContext.get_thm ctxt (Name "termination")
    2.50 -    (* FIXME avoid internal name lookup -- dynamic scoping! *)
    2.51 -  in Method.SIMPLE_METHOD (auto_term_tac ctxt intro_rule rel wfs ss) end)
    2.52 +fun relation_meth ctxt rel = 
    2.53 +    let
    2.54 +      val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
    2.55 +                 
    2.56 +      val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
    2.57 +      val rule = FundefCommon.get_termination_rule ctxt |> the
    2.58 +                  |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)
    2.59 +          
    2.60 +      val prem = #1 (Logic.dest_implies (Thm.prop_of rule))
    2.61 +      val Rvar = cert (Var (the_single (Term.add_vars prem [])))
    2.62 +    in
    2.63 +      Method.SIMPLE_METHOD (rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) 1)
    2.64 +    end
    2.65 +   
    2.66  
    2.67  val setup = Method.add_methods
    2.68 -  [("auto_term", termination_meth, "proves termination using a user-specified wellfounded relation")]
    2.69 +  [("relation", uncurry relation_meth oo Method.syntax Args.term,
    2.70 +    "proves termination using a user-specified wellfounded relation")]
    2.71  
    2.72  end
     3.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Nov 13 12:10:49 2006 +0100
     3.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Nov 13 13:51:22 2006 +0100
     3.3 @@ -20,6 +20,12 @@
     3.4  fun mk_acc domT R =
     3.5      Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R 
     3.6  
     3.7 +val function_name = suffix "C"
     3.8 +val graph_name = suffix "_graph"
     3.9 +val rel_name = suffix "_rel"
    3.10 +val dom_name = suffix "_dom"
    3.11 +
    3.12 +val dest_rel_name = unsuffix "_rel"
    3.13  
    3.14  type depgraph = int IntGraph.T
    3.15  
    3.16 @@ -216,8 +222,7 @@
    3.17      type T = thm list
    3.18      val empty = []
    3.19      val extend = I
    3.20 -    fun merge _ (l1, l2) = l1 @ l2
    3.21 -      (* FIXME exponential blowup! cf. Library.merge, Drule.merge_rules *)
    3.22 +    fun merge _ = Drule.merge_rules
    3.23      fun print  _ _ = ()
    3.24  end);
    3.25  
    3.26 @@ -230,16 +235,32 @@
    3.27  fun set_last_fundef name = FundefData.map (apfst (K name))
    3.28  fun get_last_fundef thy = fst (FundefData.get thy)
    3.29  
    3.30 +
    3.31  val map_fundef_congs = FundefCongs.map 
    3.32  val get_fundef_congs = FundefCongs.get
    3.33  
    3.34  
    3.35 +
    3.36 +structure TerminationRule = ProofDataFun
    3.37 +(struct
    3.38 +    val name = "HOL/function_def/termination"
    3.39 +    type T = thm option
    3.40 +    val init = K NONE
    3.41 +    fun print  _ _ = ()
    3.42 +end);
    3.43 +
    3.44 +val get_termination_rule = TerminationRule.get 
    3.45 +val set_termination_rule = TerminationRule.map o K o SOME
    3.46 +
    3.47 +
    3.48 +
    3.49  (* Configuration management *)
    3.50  datatype fundef_opt 
    3.51    = Sequential
    3.52    | Default of string
    3.53    | Preprocessor of string
    3.54    | Target of xstring
    3.55 +  | DomIntros
    3.56  
    3.57  datatype fundef_config
    3.58    = FundefConfig of
    3.59 @@ -247,21 +268,24 @@
    3.60      sequential: bool,
    3.61      default: string,
    3.62      preprocessor: string option,
    3.63 -    target: xstring option
    3.64 +    target: xstring option,
    3.65 +    domintros: bool
    3.66     }
    3.67  
    3.68  
    3.69 -val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, target=NONE }
    3.70 -val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, target=NONE }
    3.71 +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false }
    3.72 +val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false }
    3.73  
    3.74 -fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target}) = 
    3.75 -    FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target }
    3.76 -  | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target}) = 
    3.77 -    FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target }
    3.78 -  | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target}) = 
    3.79 -    FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target }
    3.80 -  | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target }) =
    3.81 -    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t }
    3.82 +fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros}) = 
    3.83 +    FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros }
    3.84 +  | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros}) = 
    3.85 +    FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros }
    3.86 +  | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros}) = 
    3.87 +    FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros }
    3.88 +  | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros }) =
    3.89 +    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros }
    3.90 +  | apply_opt Domintros (FundefConfig {sequential, default, preprocessor, target, domintros }) =
    3.91 +    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true }
    3.92  
    3.93  
    3.94  local structure P = OuterParse and K = OuterKeyword in
    3.95 @@ -270,6 +294,7 @@
    3.96  
    3.97  val option_parser = (P.$$$ "sequential" >> K Sequential)
    3.98                 || ((P.reserved "default" |-- P.term) >> Default)
    3.99 +               || (P.reserved "domintros" >> K DomIntros)
   3.100                 || ((P.$$$ "in" |-- P.xname) >> Target)
   3.101  
   3.102  fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") [])
   3.103 @@ -287,6 +312,12 @@
   3.104  
   3.105  
   3.106  
   3.107 +
   3.108 +
   3.109 +
   3.110 +
   3.111 +
   3.112 +
   3.113  end
   3.114  
   3.115  
     4.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Nov 13 12:10:49 2006 +0100
     4.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Nov 13 13:51:22 2006 +0100
     4.3 @@ -171,7 +171,7 @@
     4.4  
     4.5  fun termination_by_lexicographic_order name =
     4.6      FundefPackage.setup_termination_proof (SOME name)
     4.7 -    #> Proof.global_terminal_proof (Method.Basic (K LexicographicOrder.lexicographic_order), NONE)
     4.8 +    #> Proof.global_terminal_proof (Method.Basic LexicographicOrder.lexicographic_order, NONE)
     4.9  
    4.10  val setup =
    4.11      Method.add_methods [("pat_completeness", Method.no_args pat_completeness, "Completeness prover for datatype patterns")]
     5.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Mon Nov 13 12:10:49 2006 +0100
     5.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Mon Nov 13 13:51:22 2006 +0100
     5.3 @@ -10,6 +10,9 @@
     5.4  
     5.5  structure FundefLib = struct
     5.6  
     5.7 +fun plural sg pl [x] = sg
     5.8 +  | plural sg pl _ = pl
     5.9 +
    5.10  fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
    5.11  
    5.12  fun mk_forall v t = all (fastype_of v) $ lambda v t
    5.13 @@ -36,14 +39,15 @@
    5.14  (* Removes all quantifiers from a term, replacing bound variables by frees. *)
    5.15  fun dest_all_all (t as (Const ("all",_) $ _)) = 
    5.16      let
    5.17 -  val (v,b) = dest_all t
    5.18 -  val (vs, b') = dest_all_all b
    5.19 +      val (v,b) = dest_all t
    5.20 +      val (vs, b') = dest_all_all b
    5.21      in
    5.22 -  (v :: vs, b')
    5.23 +      (v :: vs, b')
    5.24      end
    5.25    | dest_all_all t = ([],t)
    5.26 +                     
    5.27  
    5.28 -
    5.29 +(* FIXME: similar to Variable.focus *)
    5.30  fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
    5.31      let
    5.32        val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
    5.33 @@ -87,12 +91,18 @@
    5.34  
    5.35  (* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *)
    5.36  fun replace_frees assoc =
    5.37 -    map_aterms (fn c as Free (n, _) => (case AList.lookup (op =) assoc n of
    5.38 -                                          NONE => c
    5.39 -                                        | SOME t => t)
    5.40 +    map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
    5.41                   | t => t)
    5.42  
    5.43  
    5.44 +fun forall_aterms P (t $ u) = forall_aterms P t andalso forall_aterms P u
    5.45 +  | forall_aterms P (Abs (_, _, t)) = forall_aterms P t
    5.46 +  | forall_aterms P a = P a
    5.47 +
    5.48 +fun exists_aterm P = not o forall_aterms (not o P)
    5.49 +
    5.50 +
    5.51 +
    5.52  
    5.53  fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b))
    5.54    | rename_bound n _ = raise Match
    5.55 @@ -100,27 +110,27 @@
    5.56  fun mk_forall_rename (n, v) =
    5.57      rename_bound n o mk_forall v 
    5.58  
    5.59 +val dummy_term = Free ("", dummyT)
    5.60 +
    5.61  fun forall_intr_rename (n, cv) thm =
    5.62      let
    5.63        val allthm = forall_intr cv thm
    5.64 -      val reflx = prop_of allthm
    5.65 -                   |> rename_bound n
    5.66 -                   |> cterm_of (theory_of_thm thm)
    5.67 -                   |> reflexive
    5.68 +      val (_, abs) = Logic.dest_all (prop_of allthm)
    5.69      in
    5.70 -      equal_elim reflx allthm
    5.71 +      Thm.rename_boundvars abs (Abs (n, dummyT, dummy_term)) allthm
    5.72      end
    5.73  
    5.74  
    5.75  (* Returns the frees in a term in canonical order, excluding the fixes from the context *)
    5.76  fun frees_in_term ctxt t =
    5.77 +    Term.add_frees t []
    5.78 +    |> filter_out (Variable.is_fixed ctxt o fst)
    5.79 +    |> rev
    5.80 +(*
    5.81      rev (fold_aterms (fn  Free (v as (x, _)) =>
    5.82                            if Variable.is_fixed ctxt x then I else insert (fn ((x, _),(y, _)) => x = y) v | _ => I) t [])
    5.83 -
    5.84 +*)
    5.85  
    5.86 -fun plural sg pl [] = sys_error "plural"
    5.87 -  | plural sg pl [x] = sg
    5.88 -  | plural sg pl (x::y::ys) = pl
    5.89  
    5.90  
    5.91  end
    5.92 \ No newline at end of file
     6.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Nov 13 12:10:49 2006 +0100
     6.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Nov 13 13:51:22 2006 +0100
     6.3 @@ -38,8 +38,6 @@
     6.4  open FundefLib
     6.5  open FundefCommon
     6.6  
     6.7 -(*fn (ctxt,s) => Variable.importT_terms (fst (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] [s])) ctxt;*)
     6.8 -
     6.9  fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
    6.10      let val (xs, ys) = split_list ps
    6.11      in xs ~~ f ys end
    6.12 @@ -64,8 +62,9 @@
    6.13      end
    6.14  
    6.15  
    6.16 -fun fundef_afterqed fixes spec mutual_info defname data [[result]] lthy =
    6.17 +fun fundef_afterqed config fixes spec mutual_info defname data [[result]] lthy =
    6.18      let
    6.19 +      val FundefConfig { domintros, ...} = config
    6.20        val Prep {f, R, ...} = data
    6.21        val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
    6.22        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    6.23 @@ -119,7 +118,7 @@
    6.24        val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) =
    6.25            FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy
    6.26  
    6.27 -      val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
    6.28 +      val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
    6.29      in
    6.30        (name, lthy
    6.31           |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
    6.32 @@ -162,6 +161,7 @@
    6.33        lthy
    6.34          |> ProofContext.note_thmss_i [(("termination",
    6.35                                          [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
    6.36 +        |> set_termination_rule termination
    6.37          |> Proof.theorem_i PureThy.internalK NONE
    6.38                             (total_termination_afterqed name data) NONE ("", [])
    6.39                             [(("", []), [(goal, [])])]
    6.40 @@ -199,9 +199,11 @@
    6.41  val setup = 
    6.42      FundefData.init 
    6.43        #> FundefCongs.init
    6.44 +      #> TerminationRule.init
    6.45        #>  Attrib.add_attributes
    6.46              [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
    6.47        #> setup_case_cong_hook
    6.48 +      #> FundefRelation.setup
    6.49  
    6.50  val get_congs = FundefCommon.get_fundef_congs o Context.Theory
    6.51  
     7.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Mon Nov 13 12:10:49 2006 +0100
     7.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Mon Nov 13 13:51:22 2006 +0100
     7.3 @@ -188,31 +188,31 @@
     7.4  (* if j < i, then turn around *)
     7.5  fun get_compat_thm thy cts i j ctxi ctxj = 
     7.6      let
     7.7 -        val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
     7.8 -        val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
     7.9 -
    7.10 -        val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
    7.11 +      val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
    7.12 +      val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
    7.13 +          
    7.14 +      val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
    7.15      in if j < i then
    7.16 -           let
    7.17 -               val compat = lookup_compat_thm j i cts
    7.18 -           in
    7.19 -               compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
    7.20 +         let
    7.21 +           val compat = lookup_compat_thm j i cts
    7.22 +         in
    7.23 +           compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
    7.24                  |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
    7.25                  |> fold implies_elim_swp agsj
    7.26                  |> fold implies_elim_swp agsi
    7.27                  |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
    7.28 -           end
    7.29 +         end
    7.30         else
    7.31 -           let
    7.32 -               val compat = lookup_compat_thm i j cts
    7.33 -           in
    7.34 +         let
    7.35 +           val compat = lookup_compat_thm i j cts
    7.36 +         in
    7.37                 compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
    7.38                   |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
    7.39                   |> fold implies_elim_swp agsi
    7.40                   |> fold implies_elim_swp agsj
    7.41                   |> implies_elim_swp (assume lhsi_eq_lhsj)
    7.42                   |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
    7.43 -           end
    7.44 +         end
    7.45      end
    7.46  
    7.47  
    7.48 @@ -237,6 +237,7 @@
    7.49                                  |> fold_rev (implies_intr o cprop_of) h_assums
    7.50                                  |> fold_rev (implies_intr o cprop_of) ags
    7.51                                  |> fold_rev forall_intr cqs
    7.52 +                                |> Drule.close_derivation
    7.53      in
    7.54        replace_lemma
    7.55      end
    7.56 @@ -364,7 +365,6 @@
    7.57                                    |> forall_intr (cterm_of thy x)
    7.58                                    |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
    7.59                                    |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
    7.60 -                                  |> Drule.close_derivation
    7.61  
    7.62          val goal = complete COMP (graph_is_function COMP conjunctionI)
    7.63                              |> Drule.close_derivation
    7.64 @@ -477,8 +477,6 @@
    7.65        val fvar = Free (fname, fT)
    7.66        val domT = domain_type fT
    7.67        val ranT = range_type fT
    7.68 -
    7.69 -                 
    7.70                              
    7.71        val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
    7.72  
    7.73 @@ -499,14 +497,14 @@
    7.74        val trees = PROFILE "making trees" (map build_tree) clauses
    7.75        val RCss = PROFILE "finding calls" (map find_calls) trees
    7.76  
    7.77 -      val ((G, GIntro_thms, G_elim), lthy) = PROFILE "def_graph" (define_graph (defname ^ "_graph") fvar domT ranT clauses RCss) lthy
    7.78 +      val ((G, GIntro_thms, G_elim), lthy) = PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
    7.79        val ((f, f_defthm), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
    7.80  
    7.81        val RCss = PROFILE "inst_RCs" (map (map (inst_RC (ProofContext.theory_of lthy) fvar f))) RCss
    7.82        val trees = PROFILE "inst_trees" (map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f)) trees
    7.83  
    7.84        val ((R, RIntro_thmss, R_elim), lthy) = 
    7.85 -          PROFILE "def_rel" (define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss) lthy
    7.86 +          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
    7.87  
    7.88        val lthy = PROFILE "abbrev"
    7.89          (snd o LocalTheory.abbrevs ("", false) (* FIXME really this mode? cf. Syntax.default_mode *)
     8.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Mon Nov 13 12:10:49 2006 +0100
     8.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Mon Nov 13 13:51:22 2006 +0100
     8.3 @@ -7,7 +7,7 @@
     8.4  
     8.5  signature LEXICOGRAPHIC_ORDER =
     8.6  sig
     8.7 -  val lexicographic_order : Method.method
     8.8 +  val lexicographic_order : Proof.context -> Method.method
     8.9    val setup: theory -> theory
    8.10  end
    8.11  
    8.12 @@ -201,10 +201,10 @@
    8.13        
    8.14  (* the main function: create table, search table, create relation,
    8.15     and prove the subgoals *)
    8.16 -fun lexicographic_order_tac (st: thm) = 
    8.17 +fun lexicographic_order_tac ctxt (st: thm) = 
    8.18      let
    8.19        val thy = theory_of_thm st
    8.20 -      val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
    8.21 +      val termination_thm = the (FundefCommon.get_termination_rule ctxt)
    8.22        val next_st = SINGLE (rtac termination_thm 1) st |> the
    8.23        val premlist = prems_of next_st
    8.24      in
    8.25 @@ -239,8 +239,8 @@
    8.26              end
    8.27      end
    8.28  
    8.29 -val lexicographic_order = Method.SIMPLE_METHOD lexicographic_order_tac
    8.30 +val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac
    8.31  
    8.32 -val setup = Method.add_methods [("lexicographic_order", Method.no_args lexicographic_order, "termination prover for lexicographic orderings")]
    8.33 +val setup = Method.add_methods [("lexicographic_order", Method.ctxt_args lexicographic_order, "termination prover for lexicographic orderings")]
    8.34  
    8.35  end
    8.36 \ No newline at end of file
     9.1 --- a/src/HOL/Tools/function_package/mutual.ML	Mon Nov 13 12:10:49 2006 +0100
     9.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Mon Nov 13 13:51:22 2006 +0100
     9.3 @@ -49,7 +49,7 @@
     9.4  (* Builds a curried clause description in abstracted form *)
     9.5  fun split_def ctxt fnames geq arities =
     9.6      let
     9.7 -      fun input_error msg = error (cat_lines [msg, ProofContext.string_of_term ctxt geq])
     9.8 +      fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
     9.9                              
    9.10        val (qs, imp) = open_all_all geq
    9.11  
    9.12 @@ -61,32 +61,27 @@
    9.13  
    9.14        val invalid_head_msg = "Head symbol of left hand side must be " ^ plural "" "one out of " fnames ^ commas_quote fnames
    9.15        val fname = fst (dest_Free head)
    9.16 -          handle TERM _ => input_error invalid_head_msg
    9.17 +          handle TERM _ => error (input_error invalid_head_msg)
    9.18  
    9.19 -      val _ = if fname mem fnames then ()
    9.20 -              else input_error invalid_head_msg
    9.21 +      val _ = assert (fname mem fnames) (input_error invalid_head_msg)
    9.22  
    9.23        fun add_bvs t is = add_loose_bnos (t, 0, is)
    9.24        val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
    9.25                    |> map (fst o nth (rev qs))
    9.26                  
    9.27 -      val _ = if null rvs then ()
    9.28 -              else input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
    9.29 -                                ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
    9.30 +      val _ = assert (null rvs) (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
    9.31 +                                              ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
    9.32  
    9.33 -      val _ = (fold o fold_aterms)
    9.34 -                 (fn Free (n, _) => if n mem fnames
    9.35 -                                    then input_error "Recursive Calls not allowed in premises:"
    9.36 -                                    else I
    9.37 -                   | _ => I) gs ()
    9.38 +      val _ = assert (forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs)
    9.39 +                     (input_error "Recursive Calls not allowed in premises")
    9.40  
    9.41        val k = length args
    9.42  
    9.43        val arities' = case Symtab.lookup arities fname of
    9.44                         NONE => Symtab.update (fname, k) arities
    9.45 -                     | SOME i => if (i <> k)
    9.46 -                                 then input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
    9.47 -                                 else arities
    9.48 +                     | SOME i => (assert (i = k)
    9.49 +                                  (input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations"));
    9.50 +                                  arities)
    9.51      in
    9.52        ((fname, qs, gs, args, rhs), arities')
    9.53      end
    10.1 --- a/src/HOL/ex/CodeCollections.thy	Mon Nov 13 12:10:49 2006 +0100
    10.2 +++ b/src/HOL/ex/CodeCollections.thy	Mon Nov 13 13:51:22 2006 +0100
    10.3 @@ -72,8 +72,6 @@
    10.4  | "abs_sorted cmp [x] = True"
    10.5  | "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))"
    10.6  
    10.7 -termination by (auto_term "measure (length o snd)")
    10.8 -
    10.9  thm abs_sorted.simps
   10.10  
   10.11  abbreviation (in ordered)
   10.12 @@ -117,8 +115,6 @@
   10.13  | "le_option' (Some x) None = False"
   10.14  | "le_option' (Some x) (Some y) = x <<= y"
   10.15  
   10.16 -termination by (auto_term "{}")
   10.17 -
   10.18  instance option :: (ordered) ordered
   10.19    "x <<= y == le_option' x y"
   10.20  proof (default, unfold ordered_option_def)
   10.21 @@ -147,7 +143,6 @@
   10.22  fun le_pair' :: "'a::ordered \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   10.23  where
   10.24    "le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
   10.25 -termination by (auto_term "{}")
   10.26  
   10.27  instance * :: (ordered, ordered) ordered
   10.28    "x <<= y == le_pair' x y"
   10.29 @@ -169,8 +164,6 @@
   10.30  | "le_list' (x#xs) [] = False"
   10.31  | "le_list' (x#xs) (y#ys) = (x << y \<or> x = y \<and> le_list' xs ys)"
   10.32  
   10.33 -termination by (auto_term "measure (length o fst)")
   10.34 -
   10.35  instance (ordered) list :: ordered
   10.36    "xs <<= ys == le_list' xs ys"
   10.37  proof (default, unfold "ordered_list_def")
    11.1 --- a/src/HOL/ex/Codegenerator.thy	Mon Nov 13 12:10:49 2006 +0100
    11.2 +++ b/src/HOL/ex/Codegenerator.thy	Mon Nov 13 13:51:22 2006 +0100
    11.3 @@ -48,7 +48,7 @@
    11.4    fac :: "int => int" where
    11.5    "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    11.6    by pat_completeness auto
    11.7 -termination by (auto_term "measure nat")
    11.8 +termination by (relation "measure nat") auto
    11.9  
   11.10  declare fac.simps [code]
   11.11  
    12.1 --- a/src/HOL/ex/Fundefs.thy	Mon Nov 13 12:10:49 2006 +0100
    12.2 +++ b/src/HOL/ex/Fundefs.thy	Mon Nov 13 13:51:22 2006 +0100
    12.3 @@ -17,8 +17,7 @@
    12.4  | "fib (Suc 0) = 1"
    12.5  | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
    12.6  
    12.7 -
    12.8 -text {* we get partial simp and induction rules: *}
    12.9 +text {* partial simp and induction rules: *}
   12.10  thm fib.psimps
   12.11  thm fib.pinduct
   12.12  
   12.13 @@ -27,15 +26,10 @@
   12.14  
   12.15  thm fib.domintros
   12.16  
   12.17 -
   12.18 -text {* Now termination: *}
   12.19 -(*termination fib
   12.20 -  by (auto_term "less_than")*)
   12.21 -
   12.22 +text {* total simp and induction rules: *}
   12.23  thm fib.simps
   12.24  thm fib.induct
   12.25  
   12.26 -
   12.27  section {* Currying *}
   12.28  
   12.29  fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   12.30 @@ -62,8 +56,7 @@
   12.31  by induct auto
   12.32  
   12.33  termination nz
   12.34 -  apply (auto_term "less_than") -- {* Oops, it left us something to prove *}
   12.35 -  by (auto simp:nz_is_zero)
   12.36 +  by (relation "less_than") (auto simp:nz_is_zero)
   12.37  
   12.38  thm nz.simps
   12.39  thm nz.induct