# HG changeset patch # User wenzelm # Date 1236955943 -3600 # Node ID 20a95d8dd7c8e186438a914d7d290dc94dbf2230 # Parent 105ad9a68e51ac8602b321832779e49019db979a# Parent b8570ea1ce25b5ed0246073ac89f9e16271ccb0f merged diff -r 105ad9a68e51 -r 20a95d8dd7c8 src/HOL/Tools/function_package/context_tree.ML --- a/src/HOL/Tools/function_package/context_tree.ML Fri Mar 13 07:35:18 2009 -0700 +++ b/src/HOL/Tools/function_package/context_tree.ML Fri Mar 13 15:52:23 2009 +0100 @@ -11,7 +11,7 @@ type ctx_tree (* FIXME: This interface is a mess and needs to be cleaned up! *) - val get_fundef_congs : Context.generic -> thm list + val get_fundef_congs : Proof.context -> thm list val add_fundef_cong : thm -> Context.generic -> Context.generic val map_fundef_congs : (thm list -> thm list) -> Context.generic -> Context.generic @@ -52,8 +52,8 @@ fun merge _ = Thm.merge_thms ); -val map_fundef_congs = FundefCongs.map -val get_fundef_congs = FundefCongs.get +val get_fundef_congs = FundefCongs.get o Context.Proof +val map_fundef_congs = FundefCongs.map val add_fundef_cong = FundefCongs.map o Thm.add_thm (* congruence rules *) @@ -127,7 +127,7 @@ fun mk_tree fvar h ctxt t = let - val congs = get_fundef_congs (Context.Proof ctxt) + val congs = get_fundef_congs ctxt val congs_deps = map (fn c => (c, cong_deps c)) (congs @ default_congs) (* FIXME: Save in theory *) fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE diff -r 105ad9a68e51 -r 20a95d8dd7c8 src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Fri Mar 13 07:35:18 2009 -0700 +++ b/src/HOL/Tools/function_package/fundef_common.ML Fri Mar 13 15:52:23 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/function_package/fundef_common.ML - ID: $Id$ Author: Alexander Krauss, TU Muenchen A package for general recursive function definitions. @@ -101,6 +100,8 @@ fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2) ); +val get_fundef = FundefData.get o Context.Proof; + (* Generally useful?? *) fun lift_morphism thy f = @@ -113,7 +114,7 @@ fun import_fundef_data t ctxt = let - val thy = Context.theory_of ctxt + val thy = ProofContext.theory_of ctxt val ct = cterm_of thy t val inst_morph = lift_morphism thy o Thm.instantiate @@ -121,20 +122,20 @@ SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) handle Pattern.MATCH => NONE in - get_first match (NetRules.retrieve (FundefData.get ctxt) t) + get_first match (NetRules.retrieve (get_fundef ctxt) t) end fun import_last_fundef ctxt = - case NetRules.rules (FundefData.get ctxt) of + case NetRules.rules (get_fundef ctxt) of [] => NONE | (t, data) :: _ => let - val ([t'], ctxt') = Variable.import_terms true [t] (Context.proof_of ctxt) + val ([t'], ctxt') = Variable.import_terms true [t] ctxt in - import_fundef_data t' (Context.Proof ctxt') + import_fundef_data t' ctxt' end -val all_fundef_data = NetRules.rules o FundefData.get +val all_fundef_data = NetRules.rules o get_fundef fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) = FundefData.map (fold (fn f => NetRules.insert (f, data)) fs) @@ -161,7 +162,7 @@ ); val set_termination_prover = TerminationProver.put -val get_termination_prover = TerminationProver.get +val get_termination_prover = TerminationProver.get o Context.Proof (* Configuration management *) diff -r 105ad9a68e51 -r 20a95d8dd7c8 src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 07:35:18 2009 -0700 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 15:52:23 2009 +0100 @@ -7,11 +7,18 @@ signature FUNDEF_DATATYPE = sig - val pat_complete_tac: Proof.context -> int -> tactic + val pat_completeness_tac: Proof.context -> int -> tactic + val pat_completeness: Proof.context -> Proof.method val prove_completeness : theory -> term list -> term -> term list list -> term list list -> thm - val pat_completeness : Proof.context -> method val setup : theory -> theory + + val add_fun : FundefCommon.fundef_config -> + (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> + bool list -> bool -> local_theory -> Proof.context + val add_fun_cmd : FundefCommon.fundef_config -> + (binding * string option * mixfix) list -> (Attrib.binding * string) list -> + bool list -> bool -> local_theory -> Proof.context end structure FundefDatatype : FUNDEF_DATATYPE = @@ -167,7 +174,7 @@ -fun pat_complete_tac ctxt = SUBGOAL (fn (subgoal, i) => +fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) => let val thy = ProofContext.theory_of ctxt val (vs, subgf) = dest_all_all subgoal @@ -196,15 +203,15 @@ handle COMPLETENESS => no_tac) -fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_complete_tac ctxt) +fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_completeness_tac ctxt) -val by_pat_completeness_simp = +val by_pat_completeness_auto = Proof.global_future_terminal_proof (Method.Basic (pat_completeness, Position.none), SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) fun termination_by method int = - FundefPackage.setup_termination_proof NONE + FundefPackage.termination_proof NONE #> Proof.global_future_terminal_proof (Method.Basic (method, Position.none), NONE) int @@ -301,24 +308,28 @@ val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), domintros=false, tailrec=false } - -local structure P = OuterParse and K = OuterKeyword in - -fun fun_cmd config fixes statements flags int lthy = +fun gen_fun add config fixes statements flags int lthy = let val group = serial_string () in lthy |> LocalTheory.set_group group - |> FundefPackage.add_fundef fixes statements config flags - |> by_pat_completeness_simp int + |> add fixes statements config flags + |> by_pat_completeness_auto int |> LocalTheory.restore |> LocalTheory.set_group group - |> termination_by (FundefCommon.get_termination_prover (Context.Proof lthy)) int + |> termination_by (FundefCommon.get_termination_prover lthy) int end; +val add_fun = gen_fun FundefPackage.add_fundef +val add_fun_cmd = gen_fun FundefPackage.add_fundef_cmd + + + +local structure P = OuterParse and K = OuterKeyword in + val _ = OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl (fundef_parser fun_config - >> (fn ((config, fixes), (flags, statements)) => fun_cmd config fixes statements flags)); + >> (fn ((config, fixes), (flags, statements)) => add_fun_cmd config fixes statements flags)); end diff -r 105ad9a68e51 -r 20a95d8dd7c8 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Fri Mar 13 07:35:18 2009 -0700 +++ b/src/HOL/Tools/function_package/fundef_package.ML Fri Mar 13 15:52:23 2009 +0100 @@ -7,24 +7,26 @@ signature FUNDEF_PACKAGE = sig - val add_fundef : (binding * string option * mixfix) list + val add_fundef : (binding * typ option * mixfix) list + -> (Attrib.binding * term) list + -> FundefCommon.fundef_config + -> bool list + -> local_theory + -> Proof.state + val add_fundef_cmd : (binding * string option * mixfix) list -> (Attrib.binding * string) list -> FundefCommon.fundef_config -> bool list -> local_theory -> Proof.state - val add_fundef_i: (binding * typ option * mixfix) list - -> (Attrib.binding * term) list - -> FundefCommon.fundef_config - -> bool list - -> local_theory - -> Proof.state - - val setup_termination_proof : string option -> local_theory -> Proof.state + val termination_proof : term option -> local_theory -> Proof.state + val termination_proof_cmd : string option -> local_theory -> Proof.state + val termination : term option -> local_theory -> Proof.state + val termination_cmd : string option -> local_theory -> Proof.state val setup : theory -> theory - val get_congs : theory -> thm list + val get_congs : Proof.context -> thm list end @@ -114,6 +116,10 @@ |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd end +val add_fundef = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) +val add_fundef_cmd = gen_add_fundef true Specification.read_spec "_::type" + + fun total_termination_afterqed data [[totality]] lthy = let val FundefCtxData { add_simps, case_names, psimps, pinducts, defname, ... } = data @@ -136,13 +142,14 @@ |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd end - -fun setup_termination_proof term_opt lthy = +fun gen_termination_proof prep_term raw_term_opt lthy = let + val term_opt = Option.map (prep_term lthy) raw_term_opt val data = the (case term_opt of - SOME t => import_fundef_data (Syntax.read_term lthy t) (Context.Proof lthy) - | NONE => import_last_fundef (Context.Proof lthy)) - handle Option.Option => error ("Not a function: " ^ quote (the_default "" term_opt)) + SOME t => (import_fundef_data t lthy + handle Option.Option => + error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) + | NONE => (import_last_fundef lthy handle Option.Option => error "Not a function")) val FundefCtxData {termination, R, ...} = data val domT = domain_type (fastype_of R) @@ -157,13 +164,18 @@ |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]] end +val termination_proof = gen_termination_proof Syntax.check_term; +val termination_proof_cmd = gen_termination_proof Syntax.read_term; + +fun termination term_opt lthy = + lthy + |> LocalTheory.set_group (serial_string ()) + |> termination_proof term_opt; + fun termination_cmd term_opt lthy = lthy |> LocalTheory.set_group (serial_string ()) - |> setup_termination_proof term_opt; - -val add_fundef = gen_add_fundef true Specification.read_spec "_::type" -val add_fundef_i = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS) + |> termination_proof_cmd term_opt; (* Datatype hook to declare datatype congs as "fundef_congs" *) @@ -180,6 +192,7 @@ val setup_case_cong = DatatypePackage.interpretation case_cong + (* setup *) val setup = @@ -190,7 +203,7 @@ #> FundefRelation.setup #> FundefCommon.TerminationSimps.setup -val get_congs = FundefCtxTree.get_fundef_congs o Context.Theory +val get_congs = FundefCtxTree.get_fundef_congs (* outer syntax *) @@ -202,7 +215,7 @@ val _ = OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal (fundef_parser default_config - >> (fn ((config, fixes), (flags, statements)) => add_fundef fixes statements config flags)); + >> (fn ((config, fixes), (flags, statements)) => add_fundef_cmd fixes statements config flags)); val _ = OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal diff -r 105ad9a68e51 -r 20a95d8dd7c8 src/HOL/Tools/function_package/induction_scheme.ML --- a/src/HOL/Tools/function_package/induction_scheme.ML Fri Mar 13 07:35:18 2009 -0700 +++ b/src/HOL/Tools/function_package/induction_scheme.ML Fri Mar 13 15:52:23 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/function_package/induction_scheme.ML - ID: $Id$ Author: Alexander Krauss, TU Muenchen A method to prove induction schemes. @@ -8,7 +7,8 @@ signature INDUCTION_SCHEME = sig val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic) - -> Proof.context -> thm list -> tactic + -> Proof.context -> thm list -> tactic + val induct_scheme_tac : Proof.context -> thm list -> tactic val setup : theory -> theory end @@ -395,8 +395,11 @@ end)) +fun induct_scheme_tac ctxt = + mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; + val setup = Method.add_methods - [("induct_scheme", Method.ctxt_args (Method.RAW_METHOD o (fn ctxt => mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt)), + [("induct_scheme", Method.ctxt_args (Method.RAW_METHOD o induct_scheme_tac), "proves an induction principle")] end diff -r 105ad9a68e51 -r 20a95d8dd7c8 src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Fri Mar 13 07:35:18 2009 -0700 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Fri Mar 13 15:52:23 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/function_package/lexicographic_order.ML - ID: $Id$ Author: Lukas Bulwahn, TU Muenchen Method for termination proofs with lexicographic orderings. @@ -7,8 +6,9 @@ signature LEXICOGRAPHIC_ORDER = sig - val lexicographic_order : thm list -> Proof.context -> Method.method - val lexicographic_order_tac : Proof.context -> tactic -> tactic + val lex_order_tac : Proof.context -> tactic -> tactic + val lexicographic_order_tac : Proof.context -> tactic + val lexicographic_order : Proof.context -> Proof.method val setup: theory -> theory end @@ -186,9 +186,10 @@ end (** The Main Function **) -fun lexicographic_order_tac ctxt solve_tac (st: thm) = + +fun lex_order_tac ctxt solve_tac (st: thm) = let - val thy = theory_of_thm st + val thy = ProofContext.theory_of ctxt val ((trueprop $ (wf $ rel)) :: tl) = prems_of st val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) @@ -213,12 +214,15 @@ THEN EVERY (map prove_row clean_table)) end -fun lexicographic_order thms ctxt = - Method.SIMPLE_METHOD (TRY (FundefCommon.apply_termination_rule ctxt 1) - THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt))) +fun lexicographic_order_tac ctxt = + TRY (FundefCommon.apply_termination_rule ctxt 1) + THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt)) + +val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac -val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order, +val setup = Method.add_methods [("lexicographic_order", Method.only_sectioned_args clasimp_modifiers lexicographic_order, "termination prover for lexicographic orderings")] - #> Context.theory_map (FundefCommon.set_termination_prover (lexicographic_order [])) + #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order) -end +end; +