--- 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
--- 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 *)
--- 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
--- 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
--- 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
--- 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;
+