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