# HG changeset patch # User krauss # Date 1163422282 -3600 # Node ID cf814e36f788d5c884161779f8b2832acfae6b6b # Parent edb595802d22e8f896db5e63ca38fa29e2daf479 replaced "auto_term" by the simpler method "relation", which does not try to simplify. Some more cleanup. diff -r edb595802d22 -r cf814e36f788 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Mon Nov 13 12:10:49 2006 +0100 +++ b/src/HOL/FunDef.thy Mon Nov 13 13:51:22 2006 +0100 @@ -199,11 +199,10 @@ use "Tools/function_package/termination.ML" use "Tools/function_package/mutual.ML" use "Tools/function_package/pattern_split.ML" +use "Tools/function_package/auto_term.ML" use "Tools/function_package/fundef_package.ML" -use "Tools/function_package/auto_term.ML" setup FundefPackage.setup -setup FundefAutoTerm.setup lemmas [fundef_cong] = let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong diff -r edb595802d22 -r cf814e36f788 src/HOL/Tools/function_package/auto_term.ML --- a/src/HOL/Tools/function_package/auto_term.ML Mon Nov 13 12:10:49 2006 +0100 +++ b/src/HOL/Tools/function_package/auto_term.ML Mon Nov 13 13:51:22 2006 +0100 @@ -3,48 +3,37 @@ Author: Alexander Krauss, TU Muenchen A package for general recursive function definitions. -The auto_term method. +Method "relation" to commence a termination proof using a user-specified relation. *) -signature FUNDEF_AUTO_TERM = +signature FUNDEF_RELATION = sig + val relation_meth : Proof.context -> term -> Method.method + val setup: theory -> theory end -structure FundefAutoTerm : FUNDEF_AUTO_TERM = +structure FundefRelation : FUNDEF_RELATION = struct -open FundefCommon -open FundefAbbrev - - -fun auto_term_tac ctxt rule rel wf_rules ss = - let - val cert = Thm.cterm_of (ProofContext.theory_of ctxt) - - val rel' = cert (singleton (Variable.polymorphic ctxt) rel) - val rule' = rule |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) - val prem = #1 (Logic.dest_implies (Thm.prop_of rule')) - val R' = cert (Var (the_single (Term.add_vars prem []))) - in - rtac (Drule.cterm_instantiate [(R', rel')] rule') 1 (* instantiate termination rule *) - THEN (ALLGOALS - (fn 1 => REPEAT (ares_tac wf_rules 1) (* Solve wellfoundedness *) - | i => asm_simp_tac ss i)) (* Simplify termination conditions *) - end - - -fun termination_meth src = Method.syntax Args.term src #> (fn (ctxt, rel) => - let - val {simps, congs, wfs} = RecdefPackage.get_hints (Context.Proof ctxt) - val ss = local_simpset_of ctxt addsimps simps - - val intro_rule = ProofContext.get_thm ctxt (Name "termination") - (* FIXME avoid internal name lookup -- dynamic scoping! *) - in Method.SIMPLE_METHOD (auto_term_tac ctxt intro_rule rel wfs ss) end) +fun relation_meth ctxt rel = + let + val cert = Thm.cterm_of (ProofContext.theory_of ctxt) + + val rel' = cert (singleton (Variable.polymorphic ctxt) rel) + val rule = FundefCommon.get_termination_rule ctxt |> the + |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) + + val prem = #1 (Logic.dest_implies (Thm.prop_of rule)) + val Rvar = cert (Var (the_single (Term.add_vars prem []))) + in + Method.SIMPLE_METHOD (rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) 1) + end + val setup = Method.add_methods - [("auto_term", termination_meth, "proves termination using a user-specified wellfounded relation")] + [("relation", uncurry relation_meth oo Method.syntax Args.term, + "proves termination using a user-specified wellfounded relation")] end diff -r edb595802d22 -r cf814e36f788 src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Mon Nov 13 12:10:49 2006 +0100 +++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Nov 13 13:51:22 2006 +0100 @@ -20,6 +20,12 @@ fun mk_acc domT R = Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R +val function_name = suffix "C" +val graph_name = suffix "_graph" +val rel_name = suffix "_rel" +val dom_name = suffix "_dom" + +val dest_rel_name = unsuffix "_rel" type depgraph = int IntGraph.T @@ -216,8 +222,7 @@ type T = thm list val empty = [] val extend = I - fun merge _ (l1, l2) = l1 @ l2 - (* FIXME exponential blowup! cf. Library.merge, Drule.merge_rules *) + fun merge _ = Drule.merge_rules fun print _ _ = () end); @@ -230,16 +235,32 @@ fun set_last_fundef name = FundefData.map (apfst (K name)) fun get_last_fundef thy = fst (FundefData.get thy) + val map_fundef_congs = FundefCongs.map val get_fundef_congs = FundefCongs.get + +structure TerminationRule = ProofDataFun +(struct + val name = "HOL/function_def/termination" + type T = thm option + val init = K NONE + fun print _ _ = () +end); + +val get_termination_rule = TerminationRule.get +val set_termination_rule = TerminationRule.map o K o SOME + + + (* Configuration management *) datatype fundef_opt = Sequential | Default of string | Preprocessor of string | Target of xstring + | DomIntros datatype fundef_config = FundefConfig of @@ -247,21 +268,24 @@ sequential: bool, default: string, preprocessor: string option, - target: xstring option + target: xstring option, + domintros: bool } -val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, target=NONE } -val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, target=NONE } +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false } +val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false } -fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target}) = - FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target } - | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target}) = - FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target } - | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target}) = - FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target } - | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target }) = - FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t } +fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros}) = + FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros } + | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros}) = + FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros } + | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros}) = + FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros } + | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros }) = + FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros } + | apply_opt Domintros (FundefConfig {sequential, default, preprocessor, target, domintros }) = + FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true } local structure P = OuterParse and K = OuterKeyword in @@ -270,6 +294,7 @@ val option_parser = (P.$$$ "sequential" >> K Sequential) || ((P.reserved "default" |-- P.term) >> Default) + || (P.reserved "domintros" >> K DomIntros) || ((P.$$$ "in" |-- P.xname) >> Target) fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") []) @@ -287,6 +312,12 @@ + + + + + + end diff -r edb595802d22 -r cf814e36f788 src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Mon Nov 13 12:10:49 2006 +0100 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Mon Nov 13 13:51:22 2006 +0100 @@ -171,7 +171,7 @@ fun termination_by_lexicographic_order name = FundefPackage.setup_termination_proof (SOME name) - #> Proof.global_terminal_proof (Method.Basic (K LexicographicOrder.lexicographic_order), NONE) + #> Proof.global_terminal_proof (Method.Basic LexicographicOrder.lexicographic_order, NONE) val setup = Method.add_methods [("pat_completeness", Method.no_args pat_completeness, "Completeness prover for datatype patterns")] diff -r edb595802d22 -r cf814e36f788 src/HOL/Tools/function_package/fundef_lib.ML --- a/src/HOL/Tools/function_package/fundef_lib.ML Mon Nov 13 12:10:49 2006 +0100 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Nov 13 13:51:22 2006 +0100 @@ -10,6 +10,9 @@ structure FundefLib = struct +fun plural sg pl [x] = sg + | plural sg pl _ = pl + fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *) fun mk_forall v t = all (fastype_of v) $ lambda v t @@ -36,14 +39,15 @@ (* Removes all quantifiers from a term, replacing bound variables by frees. *) fun dest_all_all (t as (Const ("all",_) $ _)) = let - val (v,b) = dest_all t - val (vs, b') = dest_all_all b + val (v,b) = dest_all t + val (vs, b') = dest_all_all b in - (v :: vs, b') + (v :: vs, b') end | dest_all_all t = ([],t) + - +(* FIXME: similar to Variable.focus *) fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) = let val [(n', _)] = Variable.variant_frees ctx [] [(n,T)] @@ -87,12 +91,18 @@ (* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *) fun replace_frees assoc = - map_aterms (fn c as Free (n, _) => (case AList.lookup (op =) assoc n of - NONE => c - | SOME t => t) + map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n) | t => t) +fun forall_aterms P (t $ u) = forall_aterms P t andalso forall_aterms P u + | forall_aterms P (Abs (_, _, t)) = forall_aterms P t + | forall_aterms P a = P a + +fun exists_aterm P = not o forall_aterms (not o P) + + + fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b)) | rename_bound n _ = raise Match @@ -100,27 +110,27 @@ fun mk_forall_rename (n, v) = rename_bound n o mk_forall v +val dummy_term = Free ("", dummyT) + fun forall_intr_rename (n, cv) thm = let val allthm = forall_intr cv thm - val reflx = prop_of allthm - |> rename_bound n - |> cterm_of (theory_of_thm thm) - |> reflexive + val (_, abs) = Logic.dest_all (prop_of allthm) in - equal_elim reflx allthm + Thm.rename_boundvars abs (Abs (n, dummyT, dummy_term)) allthm end (* Returns the frees in a term in canonical order, excluding the fixes from the context *) fun frees_in_term ctxt t = + Term.add_frees t [] + |> filter_out (Variable.is_fixed ctxt o fst) + |> rev +(* rev (fold_aterms (fn Free (v as (x, _)) => if Variable.is_fixed ctxt x then I else insert (fn ((x, _),(y, _)) => x = y) v | _ => I) t []) - +*) -fun plural sg pl [] = sys_error "plural" - | plural sg pl [x] = sg - | plural sg pl (x::y::ys) = pl end \ No newline at end of file diff -r edb595802d22 -r cf814e36f788 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Mon Nov 13 12:10:49 2006 +0100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Nov 13 13:51:22 2006 +0100 @@ -38,8 +38,6 @@ open FundefLib open FundefCommon -(*fn (ctxt,s) => Variable.importT_terms (fst (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] [s])) ctxt;*) - fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *) let val (xs, ys) = split_list ps in xs ~~ f ys end @@ -64,8 +62,9 @@ end -fun fundef_afterqed fixes spec mutual_info defname data [[result]] lthy = +fun fundef_afterqed config fixes spec mutual_info defname data [[result]] lthy = let + val FundefConfig { domintros, ...} = config val Prep {f, R, ...} = data val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data @@ -119,7 +118,7 @@ val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) = FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy - val afterqed = fundef_afterqed fixes spec mutual_info name prep_result + val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result in (name, lthy |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])] @@ -162,6 +161,7 @@ lthy |> ProofContext.note_thmss_i [(("termination", [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd + |> set_termination_rule termination |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name data) NONE ("", []) [(("", []), [(goal, [])])] @@ -199,9 +199,11 @@ val setup = FundefData.init #> FundefCongs.init + #> TerminationRule.init #> Attrib.add_attributes [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")] #> setup_case_cong_hook + #> FundefRelation.setup val get_congs = FundefCommon.get_fundef_congs o Context.Theory diff -r edb595802d22 -r cf814e36f788 src/HOL/Tools/function_package/fundef_prep.ML --- a/src/HOL/Tools/function_package/fundef_prep.ML Mon Nov 13 12:10:49 2006 +0100 +++ b/src/HOL/Tools/function_package/fundef_prep.ML Mon Nov 13 13:51:22 2006 +0100 @@ -188,31 +188,31 @@ (* if j < i, then turn around *) fun get_compat_thm thy cts i j ctxi ctxj = let - val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi - val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj - - val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj))) + val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi + val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj + + val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj))) in if j < i then - let - val compat = lookup_compat_thm j i cts - in - compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) + let + val compat = lookup_compat_thm j i cts + in + compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |> fold implies_elim_swp agsj |> fold implies_elim_swp agsi |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) - end + end else - let - val compat = lookup_compat_thm i j cts - in + let + val compat = lookup_compat_thm i j cts + in compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |> fold implies_elim_swp agsi |> fold implies_elim_swp agsj |> implies_elim_swp (assume lhsi_eq_lhsj) |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) - end + end end @@ -237,6 +237,7 @@ |> fold_rev (implies_intr o cprop_of) h_assums |> fold_rev (implies_intr o cprop_of) ags |> fold_rev forall_intr cqs + |> Drule.close_derivation in replace_lemma end @@ -364,7 +365,6 @@ |> forall_intr (cterm_of thy x) |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it) - |> Drule.close_derivation val goal = complete COMP (graph_is_function COMP conjunctionI) |> Drule.close_derivation @@ -477,8 +477,6 @@ val fvar = Free (fname, fT) val domT = domain_type fT val ranT = range_type fT - - val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *) @@ -499,14 +497,14 @@ val trees = PROFILE "making trees" (map build_tree) clauses val RCss = PROFILE "finding calls" (map find_calls) trees - val ((G, GIntro_thms, G_elim), lthy) = PROFILE "def_graph" (define_graph (defname ^ "_graph") fvar domT ranT clauses RCss) lthy + val ((G, GIntro_thms, G_elim), lthy) = PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy val ((f, f_defthm), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy val RCss = PROFILE "inst_RCs" (map (map (inst_RC (ProofContext.theory_of lthy) fvar f))) RCss val trees = PROFILE "inst_trees" (map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f)) trees val ((R, RIntro_thmss, R_elim), lthy) = - PROFILE "def_rel" (define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss) lthy + PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy val lthy = PROFILE "abbrev" (snd o LocalTheory.abbrevs ("", false) (* FIXME really this mode? cf. Syntax.default_mode *) diff -r edb595802d22 -r cf814e36f788 src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Mon Nov 13 12:10:49 2006 +0100 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Mon Nov 13 13:51:22 2006 +0100 @@ -7,7 +7,7 @@ signature LEXICOGRAPHIC_ORDER = sig - val lexicographic_order : Method.method + val lexicographic_order : Proof.context -> Method.method val setup: theory -> theory end @@ -201,10 +201,10 @@ (* the main function: create table, search table, create relation, and prove the subgoals *) -fun lexicographic_order_tac (st: thm) = +fun lexicographic_order_tac ctxt (st: thm) = let val thy = theory_of_thm st - val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination") + val termination_thm = the (FundefCommon.get_termination_rule ctxt) val next_st = SINGLE (rtac termination_thm 1) st |> the val premlist = prems_of next_st in @@ -239,8 +239,8 @@ end end -val lexicographic_order = Method.SIMPLE_METHOD lexicographic_order_tac +val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac -val setup = Method.add_methods [("lexicographic_order", Method.no_args lexicographic_order, "termination prover for lexicographic orderings")] +val setup = Method.add_methods [("lexicographic_order", Method.ctxt_args lexicographic_order, "termination prover for lexicographic orderings")] end \ No newline at end of file diff -r edb595802d22 -r cf814e36f788 src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Mon Nov 13 12:10:49 2006 +0100 +++ b/src/HOL/Tools/function_package/mutual.ML Mon Nov 13 13:51:22 2006 +0100 @@ -49,7 +49,7 @@ (* Builds a curried clause description in abstracted form *) fun split_def ctxt fnames geq arities = let - fun input_error msg = error (cat_lines [msg, ProofContext.string_of_term ctxt geq]) + fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq] val (qs, imp) = open_all_all geq @@ -61,32 +61,27 @@ val invalid_head_msg = "Head symbol of left hand side must be " ^ plural "" "one out of " fnames ^ commas_quote fnames val fname = fst (dest_Free head) - handle TERM _ => input_error invalid_head_msg + handle TERM _ => error (input_error invalid_head_msg) - val _ = if fname mem fnames then () - else input_error invalid_head_msg + val _ = assert (fname mem fnames) (input_error invalid_head_msg) fun add_bvs t is = add_loose_bnos (t, 0, is) val rvs = (add_bvs rhs [] \\ fold add_bvs args []) |> map (fst o nth (rev qs)) - val _ = if null rvs then () - else input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs - ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:") + val _ = assert (null rvs) (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs + ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")) - val _ = (fold o fold_aterms) - (fn Free (n, _) => if n mem fnames - then input_error "Recursive Calls not allowed in premises:" - else I - | _ => I) gs () + val _ = assert (forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs) + (input_error "Recursive Calls not allowed in premises") val k = length args val arities' = case Symtab.lookup arities fname of NONE => Symtab.update (fname, k) arities - | SOME i => if (i <> k) - then input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations") - else arities + | SOME i => (assert (i = k) + (input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")); + arities) in ((fname, qs, gs, args, rhs), arities') end diff -r edb595802d22 -r cf814e36f788 src/HOL/ex/CodeCollections.thy --- a/src/HOL/ex/CodeCollections.thy Mon Nov 13 12:10:49 2006 +0100 +++ b/src/HOL/ex/CodeCollections.thy Mon Nov 13 13:51:22 2006 +0100 @@ -72,8 +72,6 @@ | "abs_sorted cmp [x] = True" | "abs_sorted cmp (x#y#xs) = (cmp x y \ abs_sorted cmp (y#xs))" -termination by (auto_term "measure (length o snd)") - thm abs_sorted.simps abbreviation (in ordered) @@ -117,8 +115,6 @@ | "le_option' (Some x) None = False" | "le_option' (Some x) (Some y) = x <<= y" -termination by (auto_term "{}") - instance option :: (ordered) ordered "x <<= y == le_option' x y" proof (default, unfold ordered_option_def) @@ -147,7 +143,6 @@ fun le_pair' :: "'a::ordered \ 'b::ordered \ 'a \ 'b \ bool" where "le_pair' (x1, y1) (x2, y2) = (x1 << x2 \ x1 = x2 \ y1 <<= y2)" -termination by (auto_term "{}") instance * :: (ordered, ordered) ordered "x <<= y == le_pair' x y" @@ -169,8 +164,6 @@ | "le_list' (x#xs) [] = False" | "le_list' (x#xs) (y#ys) = (x << y \ x = y \ le_list' xs ys)" -termination by (auto_term "measure (length o fst)") - instance (ordered) list :: ordered "xs <<= ys == le_list' xs ys" proof (default, unfold "ordered_list_def") diff -r edb595802d22 -r cf814e36f788 src/HOL/ex/Codegenerator.thy --- a/src/HOL/ex/Codegenerator.thy Mon Nov 13 12:10:49 2006 +0100 +++ b/src/HOL/ex/Codegenerator.thy Mon Nov 13 13:51:22 2006 +0100 @@ -48,7 +48,7 @@ fac :: "int => int" where "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))" by pat_completeness auto -termination by (auto_term "measure nat") +termination by (relation "measure nat") auto declare fac.simps [code] diff -r edb595802d22 -r cf814e36f788 src/HOL/ex/Fundefs.thy --- a/src/HOL/ex/Fundefs.thy Mon Nov 13 12:10:49 2006 +0100 +++ b/src/HOL/ex/Fundefs.thy Mon Nov 13 13:51:22 2006 +0100 @@ -17,8 +17,7 @@ | "fib (Suc 0) = 1" | "fib (Suc (Suc n)) = fib n + fib (Suc n)" - -text {* we get partial simp and induction rules: *} +text {* partial simp and induction rules: *} thm fib.psimps thm fib.pinduct @@ -27,15 +26,10 @@ thm fib.domintros - -text {* Now termination: *} -(*termination fib - by (auto_term "less_than")*) - +text {* total simp and induction rules: *} thm fib.simps thm fib.induct - section {* Currying *} fun add :: "nat \ nat \ nat" @@ -62,8 +56,7 @@ by induct auto termination nz - apply (auto_term "less_than") -- {* Oops, it left us something to prove *} - by (auto simp:nz_is_zero) + by (relation "less_than") (auto simp:nz_is_zero) thm nz.simps thm nz.induct