# HG changeset patch # User wenzelm # Date 1236955806 -3600 # Node ID b8570ea1ce25b5ed0246073ac89f9e16271ccb0f # Parent cb7e886e4b1071aa0a521858f2ffc69e61eb6e7f provide regular ML interfaces for Isar source language elements; diff -r cb7e886e4b10 -r b8570ea1ce25 src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 15:50:05 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Fri Mar 13 15:50:06 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 cb7e886e4b10 -r b8570ea1ce25 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Fri Mar 13 15:50:05 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Fri Mar 13 15:50:06 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 cb7e886e4b10 -r b8570ea1ce25 src/HOL/Tools/function_package/induction_scheme.ML --- a/src/HOL/Tools/function_package/induction_scheme.ML Fri Mar 13 15:50:05 2009 +0100 +++ b/src/HOL/Tools/function_package/induction_scheme.ML Fri Mar 13 15:50:06 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 cb7e886e4b10 -r b8570ea1ce25 src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Fri Mar 13 15:50:05 2009 +0100 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Fri Mar 13 15:50:06 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; +