--- a/src/HOL/FunDef.thy Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/FunDef.thy Sun Oct 25 00:10:25 2009 +0200
@@ -9,20 +9,20 @@
uses
"Tools/prop_logic.ML"
"Tools/sat_solver.ML"
- ("Tools/Function/fundef_lib.ML")
- ("Tools/Function/fundef_common.ML")
+ ("Tools/Function/function_lib.ML")
+ ("Tools/Function/function_common.ML")
("Tools/Function/inductive_wrap.ML")
("Tools/Function/context_tree.ML")
- ("Tools/Function/fundef_core.ML")
+ ("Tools/Function/function_core.ML")
("Tools/Function/sum_tree.ML")
("Tools/Function/mutual.ML")
("Tools/Function/pattern_split.ML")
- ("Tools/Function/fundef.ML")
- ("Tools/Function/auto_term.ML")
+ ("Tools/Function/function.ML")
+ ("Tools/Function/relation.ML")
("Tools/Function/measure_functions.ML")
("Tools/Function/lexicographic_order.ML")
("Tools/Function/pat_completeness.ML")
- ("Tools/Function/fundef_datatype.ML")
+ ("Tools/Function/fun.ML")
("Tools/Function/induction_scheme.ML")
("Tools/Function/termination.ML")
("Tools/Function/decompose.ML")
@@ -104,25 +104,25 @@
"wf R \<Longrightarrow> wfP (in_rel R)"
by (simp add: wfP_def)
-use "Tools/Function/fundef_lib.ML"
-use "Tools/Function/fundef_common.ML"
+use "Tools/Function/function_lib.ML"
+use "Tools/Function/function_common.ML"
use "Tools/Function/inductive_wrap.ML"
use "Tools/Function/context_tree.ML"
-use "Tools/Function/fundef_core.ML"
+use "Tools/Function/function_core.ML"
use "Tools/Function/sum_tree.ML"
use "Tools/Function/mutual.ML"
use "Tools/Function/pattern_split.ML"
-use "Tools/Function/auto_term.ML"
-use "Tools/Function/fundef.ML"
+use "Tools/Function/relation.ML"
+use "Tools/Function/function.ML"
use "Tools/Function/pat_completeness.ML"
-use "Tools/Function/fundef_datatype.ML"
+use "Tools/Function/fun.ML"
use "Tools/Function/induction_scheme.ML"
setup {*
- Fundef.setup
+ Function.setup
#> Pat_Completeness.setup
- #> FundefDatatype.setup
- #> InductionScheme.setup
+ #> Function_Fun.setup
+ #> Induction_Scheme.setup
*}
subsection {* Measure Functions *}
@@ -142,7 +142,7 @@
by (rule is_measure_trivial)
use "Tools/Function/lexicographic_order.ML"
-setup LexicographicOrder.setup
+setup Lexicographic_Order.setup
subsection {* Congruence Rules *}
@@ -320,7 +320,7 @@
ML_val -- "setup inactive"
{*
- Context.theory_map (FundefCommon.set_termination_prover (ScnpReconstruct.decomp_scnp
+ Context.theory_map (Function_Common.set_termination_prover (ScnpReconstruct.decomp_scnp
[ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
*}
--- a/src/HOL/IsaMakefile Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/IsaMakefile Sun Oct 25 00:10:25 2009 +0200
@@ -156,15 +156,14 @@
Tools/Datatype/datatype_realizer.ML \
Tools/Datatype/datatype_rep_proofs.ML \
Tools/dseq.ML \
- Tools/Function/auto_term.ML \
Tools/Function/context_tree.ML \
Tools/Function/decompose.ML \
Tools/Function/descent.ML \
- Tools/Function/fundef_common.ML \
- Tools/Function/fundef_core.ML \
- Tools/Function/fundef_datatype.ML \
- Tools/Function/fundef_lib.ML \
- Tools/Function/fundef.ML \
+ Tools/Function/function_common.ML \
+ Tools/Function/function_core.ML \
+ Tools/Function/function_lib.ML \
+ Tools/Function/function.ML \
+ Tools/Function/fun.ML \
Tools/Function/induction_scheme.ML \
Tools/Function/inductive_wrap.ML \
Tools/Function/lexicographic_order.ML \
@@ -172,6 +171,7 @@
Tools/Function/mutual.ML \
Tools/Function/pat_completeness.ML \
Tools/Function/pattern_split.ML \
+ Tools/Function/relation.ML \
Tools/Function/scnp_reconstruct.ML \
Tools/Function/scnp_solve.ML \
Tools/Function/size.ML \
--- a/src/HOL/Library/Multiset.thy Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Library/Multiset.thy Sun Oct 25 00:10:25 2009 +0200
@@ -1607,7 +1607,7 @@
rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
val regroup_munion_conv =
- FundefLib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
+ Function_Lib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
(map (fn t => t RS eq_reflection) (@{thms union_ac} @ @{thms empty_idemp}))
fun unfold_pwleq_tac i =
--- a/src/HOL/Product_Type.thy Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Product_Type.thy Sun Oct 25 00:10:25 2009 +0200
@@ -6,7 +6,7 @@
header {* Cartesian products *}
theory Product_Type
-imports Inductive
+imports Inductive Nat
uses
("Tools/split_rule.ML")
("Tools/inductive_set.ML")
--- a/src/HOL/SizeChange/sct.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/SizeChange/sct.ML Sun Oct 25 00:10:25 2009 +0200
@@ -112,7 +112,7 @@
end
fun bind_many [] = I
- | bind_many vs = FundefLib.tupled_lambda (foldr1 HOLogic.mk_prod vs)
+ | bind_many vs = Function_Lib.tupled_lambda (foldr1 HOLogic.mk_prod vs)
(* Builds relation descriptions from a relation definition *)
fun mk_reldescs (Abs a) =
--- a/src/HOL/Tools/Function/auto_term.ML Sat Oct 24 20:27:26 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(* Title: HOL/Tools/Function/auto_term.ML
- Author: Alexander Krauss, TU Muenchen
-
-A package for general recursive function definitions.
-Method "relation" to commence a termination proof using a user-specified relation.
-*)
-
-signature FUNDEF_RELATION =
-sig
- val relation_tac: Proof.context -> term -> int -> tactic
- val setup: theory -> theory
-end
-
-structure FundefRelation : FUNDEF_RELATION =
-struct
-
-fun inst_thm ctxt rel st =
- let
- val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
- val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
- val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
- val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
- in
- Drule.cterm_instantiate [(Rvar, rel')] st'
- end
-
-fun relation_tac ctxt rel i =
- TRY (FundefCommon.apply_termination_rule ctxt i)
- THEN PRIMITIVE (inst_thm ctxt rel)
-
-val setup =
- Method.setup @{binding relation}
- (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
- "proves termination using a user-specified wellfounded relation"
-
-end
--- a/src/HOL/Tools/Function/context_tree.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/Function/context_tree.ML Sun Oct 25 00:10:25 2009 +0200
@@ -5,15 +5,15 @@
Builds and traverses trees of nested contexts along a term.
*)
-signature FUNDEF_CTXTREE =
+signature FUNCTION_CTXTREE =
sig
type ctxt = (string * typ) list * thm list (* poor man's contexts: fixes + assumes *)
type ctx_tree
(* FIXME: This interface is a mess and needs to be cleaned up! *)
- 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
+ val get_function_congs : Proof.context -> thm list
+ val add_function_cong : thm -> Context.generic -> Context.generic
+ val map_function_congs : (thm list -> thm list) -> Context.generic -> Context.generic
val cong_add: attribute
val cong_del: attribute
@@ -36,15 +36,15 @@
val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> ctx_tree -> thm * (thm * thm) list
end
-structure FundefCtxTree : FUNDEF_CTXTREE =
+structure Function_Ctx_Tree : FUNCTION_CTXTREE =
struct
type ctxt = (string * typ) list * thm list
-open FundefCommon
-open FundefLib
+open Function_Common
+open Function_Lib
-structure FundefCongs = GenericDataFun
+structure FunctionCongs = GenericDataFun
(
type T = thm list
val empty = []
@@ -52,14 +52,14 @@
fun merge _ = Thm.merge_thms
);
-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
+val get_function_congs = FunctionCongs.get o Context.Proof
+val map_function_congs = FunctionCongs.map
+val add_function_cong = FunctionCongs.map o Thm.add_thm
(* congruence rules *)
-val cong_add = Thm.declaration_attribute (map_fundef_congs o Thm.add_thm o safe_mk_meta_eq);
-val cong_del = Thm.declaration_attribute (map_fundef_congs o Thm.del_thm o safe_mk_meta_eq);
+val cong_add = Thm.declaration_attribute (map_function_congs o Thm.add_thm o safe_mk_meta_eq);
+val cong_del = Thm.declaration_attribute (map_function_congs o Thm.del_thm o safe_mk_meta_eq);
type depgraph = int IntGraph.T
@@ -128,7 +128,7 @@
fun mk_tree fvar h ctxt t =
let
- val congs = get_fundef_congs ctxt
+ val congs = get_function_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/decompose.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/Function/decompose.ML Sun Oct 25 00:10:25 2009 +0200
@@ -33,8 +33,8 @@
Const (@{const_name Set.empty}, fastype_of c1))
|> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
- val chain = case FundefLib.try_proof (cterm_of thy goal) chain_tac of
- FundefLib.Solved thm => SOME thm
+ val chain = case Function_Lib.try_proof (cterm_of thy goal) chain_tac of
+ Function_Lib.Solved thm => SOME thm
| _ => NONE
in
Termination.note_chain c1 c2 chain D
@@ -62,7 +62,7 @@
let
val is = map (fn c => find_index (curry op aconv c) cs') cs
in
- CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv is))) i
+ CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv is))) i
end)
--- a/src/HOL/Tools/Function/descent.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/Function/descent.ML Sun Oct 25 00:10:25 2009 +0200
@@ -35,7 +35,7 @@
(measures_of p) (measures_of q) D
end
in
- cont (FundefCommon.PROFILE "deriving descents" (fold derive cs) D) i
+ cont (Function_Common.PROFILE "deriving descents" (fold derive cs) D) i
end)
val derive_diag = gen_descent true
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/fun.ML Sun Oct 25 00:10:25 2009 +0200
@@ -0,0 +1,178 @@
+(* Title: HOL/Tools/Function/fun.ML
+ Author: Alexander Krauss, TU Muenchen
+
+Sequential mode for function definitions
+Command "fun" for fully automated function definitions
+*)
+
+signature FUNCTION_FUN =
+sig
+ val add_fun : Function_Common.function_config ->
+ (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
+ bool -> local_theory -> Proof.context
+ val add_fun_cmd : Function_Common.function_config ->
+ (binding * string option * mixfix) list -> (Attrib.binding * string) list ->
+ bool -> local_theory -> Proof.context
+
+ val setup : theory -> theory
+end
+
+structure Function_Fun : FUNCTION_FUN =
+struct
+
+open Function_Lib
+open Function_Common
+
+
+fun check_pats ctxt geq =
+ let
+ fun err str = error (cat_lines ["Malformed definition:",
+ str ^ " not allowed in sequential mode.",
+ Syntax.string_of_term ctxt geq])
+ val thy = ProofContext.theory_of ctxt
+
+ fun check_constr_pattern (Bound _) = ()
+ | check_constr_pattern t =
+ let
+ val (hd, args) = strip_comb t
+ in
+ (((case Datatype.info_of_constr thy (dest_Const hd) of
+ SOME _ => ()
+ | NONE => err "Non-constructor pattern")
+ handle TERM ("dest_Const", _) => err "Non-constructor patterns");
+ map check_constr_pattern args;
+ ())
+ end
+
+ val (fname, qs, gs, args, rhs) = split_def ctxt geq
+
+ val _ = if not (null gs) then err "Conditional equations" else ()
+ val _ = map check_constr_pattern args
+
+ (* just count occurrences to check linearity *)
+ val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs
+ then err "Nonlinear patterns" else ()
+ in
+ ()
+ end
+
+val by_pat_completeness_auto =
+ Proof.global_future_terminal_proof
+ (Method.Basic Pat_Completeness.pat_completeness,
+ SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
+
+fun termination_by method int =
+ Function.termination_proof NONE
+ #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
+
+fun mk_catchall fixes arity_of =
+ let
+ fun mk_eqn ((fname, fT), _) =
+ let
+ val n = arity_of fname
+ val (argTs, rT) = chop n (binder_types fT)
+ |> apsnd (fn Ts => Ts ---> body_type fT)
+
+ val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
+ in
+ HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
+ Const ("HOL.undefined", rT))
+ |> HOLogic.mk_Trueprop
+ |> fold_rev Logic.all qs
+ end
+ in
+ map mk_eqn fixes
+ end
+
+fun add_catchall ctxt fixes spec =
+ let val fqgars = map (split_def ctxt) spec
+ val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
+ |> AList.lookup (op =) #> the
+ in
+ spec @ mk_catchall fixes arity_of
+ end
+
+fun warn_if_redundant ctxt origs tss =
+ let
+ fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
+
+ val (tss', _) = chop (length origs) tss
+ fun check (t, []) = (warning (msg t); [])
+ | check (t, s) = s
+ in
+ (map check (origs ~~ tss'); tss)
+ end
+
+
+fun sequential_preproc (config as FunctionConfig {sequential, ...}) ctxt fixes spec =
+ if sequential then
+ let
+ val (bnds, eqss) = split_list spec
+
+ val eqs = map the_single eqss
+
+ val feqs = eqs
+ |> tap (check_defs ctxt fixes) (* Standard checks *)
+ |> tap (map (check_pats ctxt)) (* More checks for sequential mode *)
+
+ val compleqs = add_catchall ctxt fixes feqs (* Completion *)
+
+ val spliteqs = warn_if_redundant ctxt feqs
+ (Function_Split.split_all_equations ctxt compleqs)
+
+ fun restore_spec thms =
+ bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms)
+
+ val spliteqs' = flat (Library.take (length bnds, spliteqs))
+ val fnames = map (fst o fst) fixes
+ val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
+
+ fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
+ |> map (map snd)
+
+
+ val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding
+
+ (* using theorem names for case name currently disabled *)
+ val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es))
+ (bnds' ~~ spliteqs)
+ |> flat
+ in
+ (flat spliteqs, restore_spec, sort, case_names)
+ end
+ else
+ Function_Common.empty_preproc check_defs config ctxt fixes spec
+
+val setup =
+ Context.theory_map (Function_Common.set_preproc sequential_preproc)
+
+
+val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*),
+ domintros=false, partials=false, tailrec=false }
+
+fun gen_fun add config fixes statements int lthy =
+ let val group = serial_string () in
+ lthy
+ |> LocalTheory.set_group group
+ |> add fixes statements config
+ |> by_pat_completeness_auto int
+ |> LocalTheory.restore
+ |> LocalTheory.set_group group
+ |> termination_by (Function_Common.get_termination_prover lthy) int
+ end;
+
+val add_fun = gen_fun Function.add_function
+val add_fun_cmd = gen_fun Function.add_function_cmd
+
+
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val _ =
+ OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
+ (function_parser fun_config
+ >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements));
+
+end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/function.ML Sun Oct 25 00:10:25 2009 +0200
@@ -0,0 +1,227 @@
+(* Title: HOL/Tools/Function/fundef.ML
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+Isar commands.
+*)
+
+signature FUNCTION =
+sig
+ val add_function : (binding * typ option * mixfix) list
+ -> (Attrib.binding * term) list
+ -> Function_Common.function_config
+ -> local_theory
+ -> Proof.state
+ val add_function_cmd : (binding * string option * mixfix) list
+ -> (Attrib.binding * string) list
+ -> Function_Common.function_config
+ -> 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 : Proof.context -> thm list
+end
+
+
+structure Function : FUNCTION =
+struct
+
+open Function_Lib
+open Function_Common
+
+val simp_attribs = map (Attrib.internal o K)
+ [Simplifier.simp_add,
+ Code.add_default_eqn_attribute,
+ Nitpick_Simps.add,
+ Quickcheck_RecFun_Simps.add]
+
+val psimp_attribs = map (Attrib.internal o K)
+ [Simplifier.simp_add,
+ Nitpick_Psimps.add]
+
+fun note_theorem ((name, atts), ths) =
+ LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
+
+fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
+
+fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
+ let
+ val spec = post simps
+ |> map (apfst (apsnd (fn ats => moreatts @ ats)))
+ |> map (apfst (apfst extra_qualify))
+
+ val (saved_spec_simps, lthy) =
+ fold_map (LocalTheory.note Thm.generatedK) spec lthy
+
+ val saved_simps = maps snd saved_spec_simps
+ val simps_by_f = sort saved_simps
+
+ fun add_for_f fname simps =
+ note_theorem ((Long_Name.qualify fname label, []), simps) #> snd
+ in
+ (saved_simps,
+ fold2 add_for_f fnames simps_by_f lthy)
+ end
+
+fun gen_add_function is_external prep default_constraint fixspec eqns config lthy =
+ let
+ val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
+ val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
+ val fixes = map (apfst (apfst Binding.name_of)) fixes0;
+ val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
+ val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
+
+ val defname = mk_defname fixes
+ val FunctionConfig {partials, ...} = config
+
+ val ((goalstate, cont), lthy) =
+ Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
+
+ fun afterqed [[proof]] lthy =
+ let
+ val FunctionResult {fs, R, psimps, trsimps, simple_pinducts, termination,
+ domintros, cases, ...} =
+ cont (Thm.close_derivation proof)
+
+ val fnames = map (fst o fst) fixes
+ val qualify = Long_Name.qualify defname
+ val addsmps = add_simps fnames post sort_cont
+
+ val (((psimps', pinducts'), (_, [termination'])), lthy) =
+ lthy
+ |> addsmps (Binding.qualify false "partial") "psimps"
+ psimp_attribs psimps
+ ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
+ ||>> note_theorem ((qualify "pinduct",
+ [Attrib.internal (K (RuleCases.case_names cnames)),
+ Attrib.internal (K (RuleCases.consumes 1)),
+ Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
+ ||>> note_theorem ((qualify "termination", []), [termination])
+ ||> (snd o note_theorem ((qualify "cases",
+ [Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
+ ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
+
+ val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
+ pinducts=snd pinducts', termination=termination',
+ fs=fs, R=R, defname=defname }
+ val _ =
+ if not is_external then ()
+ else Specification.print_consts lthy (K false) (map fst fixes)
+ in
+ lthy
+ |> LocalTheory.declaration (add_function_data o morph_function_data cdata)
+ end
+ in
+ lthy
+ |> is_external ? LocalTheory.set_group (serial_string ())
+ |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
+ |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
+ end
+
+val add_function = gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
+
+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_function_data t lthy
+ handle Option.Option =>
+ error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
+ | NONE => (import_last_function lthy handle Option.Option => error "Not a function"))
+
+ val FunctionCtxData { termination, R, add_simps, case_names, psimps,
+ pinducts, defname, ...} = data
+ val domT = domain_type (fastype_of R)
+ val goal = HOLogic.mk_Trueprop
+ (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
+ fun afterqed [[totality]] lthy =
+ let
+ val totality = Thm.close_derivation totality
+ val remove_domain_condition =
+ full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
+ val tsimps = map remove_domain_condition psimps
+ val tinduct = map remove_domain_condition pinducts
+ val qualify = Long_Name.qualify defname;
+ in
+ lthy
+ |> add_simps I "simps" simp_attribs tsimps |> snd
+ |> note_theorem
+ ((qualify "induct",
+ [Attrib.internal (K (RuleCases.case_names case_names))]),
+ tinduct) |> snd
+ end
+ in
+ lthy
+ |> ProofContext.note_thmss ""
+ [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
+ |> ProofContext.note_thmss ""
+ [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
+ |> ProofContext.note_thmss ""
+ [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
+ [([Goal.norm_result termination], [])])] |> snd
+ |> Proof.theorem_i NONE afterqed [[(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 ())
+ |> termination_proof_cmd term_opt;
+
+
+(* Datatype hook to declare datatype congs as "function_congs" *)
+
+
+fun add_case_cong n thy =
+ Context.theory_map (Function_Ctx_Tree.map_function_congs (Thm.add_thm
+ (Datatype.the_info thy n
+ |> #case_cong
+ |> safe_mk_meta_eq)))
+ thy
+
+val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
+
+
+(* setup *)
+
+val setup =
+ Attrib.setup @{binding fundef_cong}
+ (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
+ "declaration of congruence rule for function definitions"
+ #> setup_case_cong
+ #> Function_Relation.setup
+ #> Function_Common.Termination_Simps.setup
+
+val get_congs = Function_Ctx_Tree.get_function_congs
+
+
+(* outer syntax *)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val _ =
+ OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
+ (function_parser default_config
+ >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config));
+
+val _ =
+ OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
+ (Scan.option P.term >> termination_cmd);
+
+end;
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/function_common.ML Sun Oct 25 00:10:25 2009 +0200
@@ -0,0 +1,348 @@
+(* Title: HOL/Tools/Function/fundef_common.ML
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+Common definitions and other infrastructure.
+*)
+
+structure Function_Common =
+struct
+
+local open Function_Lib in
+
+(* Profiling *)
+val profile = Unsynchronized.ref false;
+
+fun PROFILE msg = if !profile then timeap_msg msg else I
+
+
+val acc_const_name = @{const_name accp}
+fun mk_acc domT R =
+ Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R
+
+val function_name = suffix "C"
+val graph_name = suffix "_graph"
+val rel_name = suffix "_rel"
+val dom_name = suffix "_dom"
+
+(* Termination rules *)
+
+structure TerminationRule = GenericDataFun
+(
+ type T = thm list
+ val empty = []
+ val extend = I
+ fun merge _ = Thm.merge_thms
+);
+
+val get_termination_rules = TerminationRule.get
+val store_termination_rule = TerminationRule.map o cons
+val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
+
+
+(* Function definition result data *)
+
+datatype function_result =
+ FunctionResult of
+ {
+ fs: term list,
+ G: term,
+ R: term,
+
+ psimps : thm list,
+ trsimps : thm list option,
+
+ simple_pinducts : thm list,
+ cases : thm,
+ termination : thm,
+ domintros : thm list option
+ }
+
+
+datatype function_context_data =
+ FunctionCtxData of
+ {
+ defname : string,
+
+ (* contains no logical entities: invariant under morphisms *)
+ add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list
+ -> local_theory -> thm list * local_theory,
+ case_names : string list,
+
+ fs : term list,
+ R : term,
+
+ psimps: thm list,
+ pinducts: thm list,
+ termination: thm
+ }
+
+fun morph_function_data (FunctionCtxData {add_simps, case_names, fs, R,
+ psimps, pinducts, termination, defname}) phi =
+ let
+ val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
+ val name = Binding.name_of o Morphism.binding phi o Binding.name
+ in
+ FunctionCtxData { add_simps = add_simps, case_names = case_names,
+ fs = map term fs, R = term R, psimps = fact psimps,
+ pinducts = fact pinducts, termination = thm termination,
+ defname = name defname }
+ end
+
+structure FunctionData = GenericDataFun
+(
+ type T = (term * function_context_data) Item_Net.T;
+ val empty = Item_Net.init
+ (op aconv o pairself fst : (term * function_context_data) * (term * function_context_data) -> bool)
+ fst;
+ val copy = I;
+ val extend = I;
+ fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
+);
+
+val get_function = FunctionData.get o Context.Proof;
+
+
+(* Generally useful?? *)
+fun lift_morphism thy f =
+ let
+ val term = Drule.term_rule thy f
+ in
+ Morphism.thm_morphism f $> Morphism.term_morphism term
+ $> Morphism.typ_morphism (Logic.type_map term)
+ end
+
+fun import_function_data t ctxt =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val ct = cterm_of thy t
+ val inst_morph = lift_morphism thy o Thm.instantiate
+
+ fun match (trm, data) =
+ SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
+ handle Pattern.MATCH => NONE
+ in
+ get_first match (Item_Net.retrieve (get_function ctxt) t)
+ end
+
+fun import_last_function ctxt =
+ case Item_Net.content (get_function ctxt) of
+ [] => NONE
+ | (t, data) :: _ =>
+ let
+ val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+ in
+ import_function_data t' ctxt'
+ end
+
+val all_function_data = Item_Net.content o get_function
+
+fun add_function_data (data as FunctionCtxData {fs, termination, ...}) =
+ FunctionData.map (fold (fn f => Item_Net.insert (f, data)) fs)
+ #> store_termination_rule termination
+
+
+(* Simp rules for termination proofs *)
+
+structure Termination_Simps = Named_Thms
+(
+ val name = "termination_simp"
+ val description = "Simplification rule for termination proofs"
+);
+
+
+(* Default Termination Prover *)
+
+structure TerminationProver = GenericDataFun
+(
+ type T = Proof.context -> Proof.method
+ val empty = (fn _ => error "Termination prover not configured")
+ val extend = I
+ fun merge _ (a,b) = b (* FIXME *)
+);
+
+val set_termination_prover = TerminationProver.put
+val get_termination_prover = TerminationProver.get o Context.Proof
+
+
+(* Configuration management *)
+datatype function_opt
+ = Sequential
+ | Default of string
+ | DomIntros
+ | No_Partials
+ | Tailrec
+
+datatype function_config
+ = FunctionConfig of
+ {
+ sequential: bool,
+ default: string,
+ domintros: bool,
+ partials: bool,
+ tailrec: bool
+ }
+
+fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
+ FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec}
+ | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
+ FunctionConfig {sequential=sequential, default=d, domintros=domintros, partials=partials, tailrec=tailrec}
+ | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
+ FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials, tailrec=tailrec}
+ | apply_opt Tailrec (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
+ FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=partials, tailrec=true}
+ | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
+ FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false, tailrec=true}
+
+val default_config =
+ FunctionConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*),
+ domintros=false, partials=true, tailrec=false }
+
+
+(* Analyzing function equations *)
+
+fun split_def ctxt geq =
+ let
+ fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
+ val qs = Term.strip_qnt_vars "all" geq
+ val imp = Term.strip_qnt_body "all" geq
+ val (gs, eq) = Logic.strip_horn imp
+
+ val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
+ handle TERM _ => error (input_error "Not an equation")
+
+ val (head, args) = strip_comb f_args
+
+ val fname = fst (dest_Free head)
+ handle TERM _ => error (input_error "Head symbol must not be a bound variable")
+ in
+ (fname, qs, gs, args, rhs)
+ end
+
+(* Check for all sorts of errors in the input *)
+fun check_defs ctxt fixes eqs =
+ let
+ val fnames = map (fst o fst) fixes
+
+ fun check geq =
+ let
+ fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
+
+ val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
+
+ val _ = fname mem fnames
+ orelse input_error
+ ("Head symbol of left hand side must be "
+ ^ plural "" "one out of " fnames ^ commas_quote fnames)
+
+ val _ = length args > 0 orelse input_error "Function has no arguments:"
+
+ fun add_bvs t is = add_loose_bnos (t, 0, is)
+ val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
+ |> map (fst o nth (rev qs))
+
+ val _ = null rvs orelse input_error
+ ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
+ ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
+
+ val _ = forall (not o Term.exists_subterm
+ (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
+ orelse input_error "Defined function may not occur in premises or arguments"
+
+ val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
+ val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
+ val _ = null funvars
+ orelse (warning (cat_lines
+ ["Bound variable" ^ plural " " "s " funvars
+ ^ commas_quote (map fst funvars) ^
+ " occur" ^ plural "s" "" funvars ^ " in function position.",
+ "Misspelled constructor???"]); true)
+ in
+ (fname, length args)
+ end
+
+ val _ = AList.group (op =) (map check eqs)
+ |> map (fn (fname, ars) =>
+ length (distinct (op =) ars) = 1
+ orelse error ("Function " ^ quote fname ^
+ " has different numbers of arguments in different equations"))
+
+ fun check_sorts ((fname, fT), _) =
+ Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
+ orelse error (cat_lines
+ ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
+ setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
+
+ val _ = map check_sorts fixes
+ in
+ ()
+ end
+
+(* Preprocessors *)
+
+type fixes = ((string * typ) * mixfix) list
+type 'a spec = (Attrib.binding * 'a list) list
+type preproc = function_config -> Proof.context -> fixes -> term spec
+ -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
+
+val fname_of = fst o dest_Free o fst o strip_comb o fst
+ o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
+
+fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
+ | mk_case_names _ n 0 = []
+ | mk_case_names _ n 1 = [n]
+ | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
+
+fun empty_preproc check _ ctxt fixes spec =
+ let
+ val (bnds, tss) = split_list spec
+ val ts = flat tss
+ val _ = check ctxt fixes ts
+ val fnames = map (fst o fst) fixes
+ val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
+
+ fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1)
+ (indices ~~ xs)
+ |> map (map snd)
+
+ (* using theorem names for case name currently disabled *)
+ val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
+ in
+ (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
+ end
+
+structure Preprocessor = GenericDataFun
+(
+ type T = preproc
+ val empty : T = empty_preproc check_defs
+ val extend = I
+ fun merge _ (a, _) = a
+);
+
+val get_preproc = Preprocessor.get o Context.Proof
+val set_preproc = Preprocessor.map o K
+
+
+
+local
+ structure P = OuterParse and K = OuterKeyword
+
+ val option_parser =
+ P.group "option" ((P.reserved "sequential" >> K Sequential)
+ || ((P.reserved "default" |-- P.term) >> Default)
+ || (P.reserved "domintros" >> K DomIntros)
+ || (P.reserved "no_partials" >> K No_Partials)
+ || (P.reserved "tailrec" >> K Tailrec))
+
+ fun config_parser default =
+ (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
+ >> (fn opts => fold apply_opt opts default)
+in
+ fun function_parser default_cfg =
+ config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
+end
+
+
+end
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/function_core.ML Sun Oct 25 00:10:25 2009 +0200
@@ -0,0 +1,956 @@
+(* Title: HOL/Tools/Function/function_core.ML
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions:
+Main functionality.
+*)
+
+signature FUNCTION_CORE =
+sig
+ val trace: bool Unsynchronized.ref
+
+ val prepare_function : Function_Common.function_config
+ -> string (* defname *)
+ -> ((bstring * typ) * mixfix) list (* defined symbol *)
+ -> ((bstring * typ) list * term list * term * term) list (* specification *)
+ -> local_theory
+
+ -> (term (* f *)
+ * thm (* goalstate *)
+ * (thm -> Function_Common.function_result) (* continuation *)
+ ) * local_theory
+
+end
+
+structure Function_Core : FUNCTION_CORE =
+struct
+
+val trace = Unsynchronized.ref false;
+fun trace_msg msg = if ! trace then tracing (msg ()) else ();
+
+val boolT = HOLogic.boolT
+val mk_eq = HOLogic.mk_eq
+
+open Function_Lib
+open Function_Common
+
+datatype globals =
+ Globals of {
+ fvar: term,
+ domT: typ,
+ ranT: typ,
+ h: term,
+ y: term,
+ x: term,
+ z: term,
+ a: term,
+ P: term,
+ D: term,
+ Pbool:term
+}
+
+
+datatype rec_call_info =
+ RCInfo of
+ {
+ RIvs: (string * typ) list, (* Call context: fixes and assumes *)
+ CCas: thm list,
+ rcarg: term, (* The recursive argument *)
+
+ llRI: thm,
+ h_assum: term
+ }
+
+
+datatype clause_context =
+ ClauseContext of
+ {
+ ctxt : Proof.context,
+
+ qs : term list,
+ gs : term list,
+ lhs: term,
+ rhs: term,
+
+ cqs: cterm list,
+ ags: thm list,
+ case_hyp : thm
+ }
+
+
+fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
+ ClauseContext { ctxt = ProofContext.transfer thy ctxt,
+ qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
+
+
+datatype clause_info =
+ ClauseInfo of
+ {
+ no: int,
+ qglr : ((string * typ) list * term list * term * term),
+ cdata : clause_context,
+
+ tree: Function_Ctx_Tree.ctx_tree,
+ lGI: thm,
+ RCs: rec_call_info list
+ }
+
+
+(* Theory dependencies. *)
+val Pair_inject = @{thm Product_Type.Pair_inject};
+
+val acc_induct_rule = @{thm accp_induct_rule};
+
+val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
+val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness};
+val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff};
+
+val acc_downward = @{thm accp_downward};
+val accI = @{thm accp.accI};
+val case_split = @{thm HOL.case_split};
+val fundef_default_value = @{thm FunDef.fundef_default_value};
+val not_acc_down = @{thm not_accp_down};
+
+
+
+fun find_calls tree =
+ let
+ fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
+ | add_Ri _ _ _ _ = raise Match
+ in
+ rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
+ end
+
+
+(** building proof obligations *)
+
+fun mk_compat_proof_obligations domT ranT fvar f glrs =
+ let
+ fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
+ let
+ val shift = incr_boundvars (length qs')
+ in
+ Logic.mk_implies
+ (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
+ HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
+ |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
+ |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
+ |> curry abstract_over fvar
+ |> curry subst_bound f
+ end
+ in
+ map mk_impl (unordered_pairs glrs)
+ end
+
+
+fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
+ let
+ fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
+ HOLogic.mk_Trueprop Pbool
+ |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+ in
+ HOLogic.mk_Trueprop Pbool
+ |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
+ |> mk_forall_rename ("x", x)
+ |> mk_forall_rename ("P", Pbool)
+ end
+
+(** making a context with it's own local bindings **)
+
+fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
+ let
+ val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
+ |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
+
+ val thy = ProofContext.theory_of ctxt'
+
+ fun inst t = subst_bounds (rev qs, t)
+ val gs = map inst pre_gs
+ val lhs = inst pre_lhs
+ val rhs = inst pre_rhs
+
+ val cqs = map (cterm_of thy) qs
+ val ags = map (assume o cterm_of thy) gs
+
+ val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
+ in
+ ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
+ cqs = cqs, ags = ags, case_hyp = case_hyp }
+ end
+
+
+(* lowlevel term function. FIXME: remove *)
+fun abstract_over_list vs body =
+ let
+ fun abs lev v tm =
+ if v aconv tm then Bound lev
+ else
+ (case tm of
+ Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
+ | t $ u => abs lev v t $ abs lev v u
+ | t => t);
+ in
+ fold_index (fn (i, v) => fn t => abs i v t) vs body
+ end
+
+
+
+fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
+ let
+ val Globals {h, fvar, x, ...} = globals
+
+ val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
+ val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+
+ (* Instantiate the GIntro thm with "f" and import into the clause context. *)
+ val lGI = GIntro_thm
+ |> forall_elim (cert f)
+ |> fold forall_elim cqs
+ |> fold Thm.elim_implies ags
+
+ fun mk_call_info (rcfix, rcassm, rcarg) RI =
+ let
+ val llRI = RI
+ |> fold forall_elim cqs
+ |> fold (forall_elim o cert o Free) rcfix
+ |> fold Thm.elim_implies ags
+ |> fold Thm.elim_implies rcassm
+
+ val h_assum =
+ HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
+ |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ |> fold_rev (Logic.all o Free) rcfix
+ |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
+ |> abstract_over_list (rev qs)
+ in
+ RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
+ end
+
+ val RC_infos = map2 mk_call_info RCs RIntro_thms
+ in
+ ClauseInfo
+ {
+ no=no,
+ cdata=cdata,
+ qglr=qglr,
+
+ lGI=lGI,
+ RCs=RC_infos,
+ tree=tree
+ }
+ end
+
+
+
+
+
+
+
+(* replace this by a table later*)
+fun store_compat_thms 0 thms = []
+ | store_compat_thms n thms =
+ let
+ val (thms1, thms2) = chop n thms
+ in
+ (thms1 :: store_compat_thms (n - 1) thms2)
+ end
+
+(* expects i <= j *)
+fun lookup_compat_thm i j cts =
+ nth (nth cts (i - 1)) (j - i)
+
+(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
+(* 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 (HOLogic.mk_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" *)
+ |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
+ |> fold Thm.elim_implies agsj
+ |> fold Thm.elim_implies agsi
+ |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
+ end
+ else
+ 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 Thm.elim_implies agsi
+ |> fold Thm.elim_implies agsj
+ |> Thm.elim_implies (assume lhsi_eq_lhsj)
+ |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
+ end
+ end
+
+
+
+
+(* Generates the replacement lemma in fully quantified form. *)
+fun mk_replacement_lemma thy h ih_elim clause =
+ let
+ val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
+ local open Conv in
+ val ih_conv = arg1_conv o arg_conv o arg_conv
+ end
+
+ val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
+
+ val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
+ val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
+
+ val (eql, _) = Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
+
+ val replace_lemma = (eql RS meta_eq_to_obj_eq)
+ |> implies_intr (cprop_of case_hyp)
+ |> fold_rev (implies_intr o cprop_of) h_assums
+ |> fold_rev (implies_intr o cprop_of) ags
+ |> fold_rev forall_intr cqs
+ |> Thm.close_derivation
+ in
+ replace_lemma
+ end
+
+
+fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
+ let
+ val Globals {h, y, x, fvar, ...} = globals
+ val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
+ val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
+
+ val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
+ = mk_clause_context x ctxti cdescj
+
+ val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
+ val compat = get_compat_thm thy compat_store i j cctxi cctxj
+ val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
+
+ val RLj_import =
+ RLj |> fold forall_elim cqsj'
+ |> fold Thm.elim_implies agsj'
+ |> fold Thm.elim_implies Ghsj'
+
+ val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
+ val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
+ in
+ (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
+ |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
+ |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
+ |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
+ |> fold_rev (implies_intr o cprop_of) Ghsj'
+ |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
+ |> implies_intr (cprop_of y_eq_rhsj'h)
+ |> implies_intr (cprop_of lhsi_eq_lhsj')
+ |> fold_rev forall_intr (cterm_of thy h :: cqsj')
+ end
+
+
+
+fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
+ let
+ val Globals {x, y, ranT, fvar, ...} = globals
+ val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
+ val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
+
+ val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
+
+ fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
+ |> fold_rev (implies_intr o cprop_of) CCas
+ |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+
+ val existence = fold (curry op COMP o prep_RC) RCs lGI
+
+ val P = cterm_of thy (mk_eq (y, rhsC))
+ val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
+
+ val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
+
+ val uniqueness = G_cases
+ |> forall_elim (cterm_of thy lhs)
+ |> forall_elim (cterm_of thy y)
+ |> forall_elim P
+ |> Thm.elim_implies G_lhs_y
+ |> fold Thm.elim_implies unique_clauses
+ |> implies_intr (cprop_of G_lhs_y)
+ |> forall_intr (cterm_of thy y)
+
+ val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
+
+ val exactly_one =
+ ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
+ |> curry (op COMP) existence
+ |> curry (op COMP) uniqueness
+ |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
+ |> implies_intr (cprop_of case_hyp)
+ |> fold_rev (implies_intr o cprop_of) ags
+ |> fold_rev forall_intr cqs
+
+ val function_value =
+ existence
+ |> implies_intr ihyp
+ |> implies_intr (cprop_of case_hyp)
+ |> forall_intr (cterm_of thy x)
+ |> forall_elim (cterm_of thy lhs)
+ |> curry (op RS) refl
+ in
+ (exactly_one, function_value)
+ end
+
+
+
+
+fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
+ let
+ val Globals {h, domT, ranT, x, ...} = globals
+ val thy = ProofContext.theory_of ctxt
+
+ (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
+ val ihyp = Term.all domT $ Abs ("z", domT,
+ Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
+ HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
+ Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
+ |> cterm_of thy
+
+ val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
+ val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
+ val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
+ |> instantiate' [] [NONE, SOME (cterm_of thy h)]
+
+ val _ = trace_msg (K "Proving Replacement lemmas...")
+ val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
+
+ val _ = trace_msg (K "Proving cases for unique existence...")
+ val (ex1s, values) =
+ split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
+
+ val _ = trace_msg (K "Proving: Graph is a function")
+ val graph_is_function = complete
+ |> Thm.forall_elim_vars 0
+ |> fold (curry op COMP) ex1s
+ |> implies_intr (ihyp)
+ |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
+ |> 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 o Var) (Term.add_vars (prop_of it) []) it)
+
+ val goalstate = Conjunction.intr graph_is_function complete
+ |> Thm.close_derivation
+ |> Goal.protect
+ |> fold_rev (implies_intr o cprop_of) compat
+ |> implies_intr (cprop_of complete)
+ in
+ (goalstate, values)
+ end
+
+
+fun define_graph Gname fvar domT ranT clauses RCss lthy =
+ let
+ val GT = domT --> ranT --> boolT
+ val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
+
+ fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
+ let
+ fun mk_h_assm (rcfix, rcassm, rcarg) =
+ HOLogic.mk_Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
+ |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ |> fold_rev (Logic.all o Free) rcfix
+ in
+ HOLogic.mk_Trueprop (Gvar $ lhs $ rhs)
+ |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> fold_rev Logic.all (fvar :: qs)
+ end
+
+ val G_intros = map2 mk_GIntro clauses RCss
+
+ val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
+ Function_Inductive_Wrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
+ in
+ ((G, GIntro_thms, G_elim, G_induct), lthy)
+ end
+
+
+
+fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
+ let
+ val f_def =
+ Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
+ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
+ |> Syntax.check_term lthy
+
+ val ((f, (_, f_defthm)), lthy) =
+ LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy
+ in
+ ((f, f_defthm), lthy)
+ end
+
+
+fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
+ let
+
+ val RT = domT --> domT --> boolT
+ val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
+
+ fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
+ HOLogic.mk_Trueprop (Rvar $ rcarg $ lhs)
+ |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> fold_rev (Logic.all o Free) rcfix
+ |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+ (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
+
+ val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
+
+ val (RIntro_thmss, (R, R_elim, _, lthy)) =
+ fold_burrow Function_Inductive_Wrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
+ in
+ ((R, RIntro_thmss, R_elim), lthy)
+ end
+
+
+fun fix_globals domT ranT fvar ctxt =
+ let
+ val ([h, y, x, z, a, D, P, Pbool],ctxt') =
+ Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
+ in
+ (Globals {h = Free (h, domT --> ranT),
+ y = Free (y, ranT),
+ x = Free (x, domT),
+ z = Free (z, domT),
+ a = Free (a, domT),
+ D = Free (D, domT --> boolT),
+ P = Free (P, domT --> boolT),
+ Pbool = Free (Pbool, boolT),
+ fvar = fvar,
+ domT = domT,
+ ranT = ranT
+ },
+ ctxt')
+ end
+
+
+
+fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
+ let
+ fun inst_term t = subst_bound(f, abstract_over (fvar, t))
+ in
+ (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
+ end
+
+
+
+(**********************************************************
+ * PROVING THE RULES
+ **********************************************************)
+
+fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
+ let
+ val Globals {domT, z, ...} = globals
+
+ fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
+ let
+ val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
+ val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
+ in
+ ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
+ |> (fn it => it COMP graph_is_function)
+ |> implies_intr z_smaller
+ |> forall_intr (cterm_of thy z)
+ |> (fn it => it COMP valthm)
+ |> implies_intr lhs_acc
+ |> asm_simplify (HOL_basic_ss addsimps [f_iff])
+ |> fold_rev (implies_intr o cprop_of) ags
+ |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+ end
+ in
+ map2 mk_psimp clauses valthms
+ end
+
+
+(** Induction rule **)
+
+
+val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
+
+
+fun mk_partial_induct_rule thy globals R complete_thm clauses =
+ let
+ val Globals {domT, x, z, a, P, D, ...} = globals
+ val acc_R = mk_acc domT R
+
+ val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
+ val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
+
+ val D_subset = cterm_of thy (Logic.all x
+ (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
+
+ val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
+ Logic.all x
+ (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
+ Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
+ HOLogic.mk_Trueprop (D $ z)))))
+ |> cterm_of thy
+
+
+ (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
+ val ihyp = Term.all domT $ Abs ("z", domT,
+ Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
+ HOLogic.mk_Trueprop (P $ Bound 0)))
+ |> cterm_of thy
+
+ val aihyp = assume ihyp
+
+ fun prove_case clause =
+ let
+ val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
+ qglr = (oqs, _, _, _), ...} = clause
+
+ val case_hyp_conv = K (case_hyp RS eq_reflection)
+ local open Conv in
+ val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
+ val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
+ end
+
+ fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
+ sih |> forall_elim (cterm_of thy rcarg)
+ |> Thm.elim_implies llRI
+ |> fold_rev (implies_intr o cprop_of) CCas
+ |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+
+ val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
+
+ val step = HOLogic.mk_Trueprop (P $ lhs)
+ |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
+ |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+ |> cterm_of thy
+
+ val P_lhs = assume step
+ |> fold forall_elim cqs
+ |> Thm.elim_implies lhs_D
+ |> fold Thm.elim_implies ags
+ |> fold Thm.elim_implies P_recs
+
+ val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
+ |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
+ |> symmetric (* P lhs == P x *)
+ |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
+ |> implies_intr (cprop_of case_hyp)
+ |> fold_rev (implies_intr o cprop_of) ags
+ |> fold_rev forall_intr cqs
+ in
+ (res, step)
+ end
+
+ val (cases, steps) = split_list (map prove_case clauses)
+
+ val istep = complete_thm
+ |> Thm.forall_elim_vars 0
+ |> fold (curry op COMP) cases (* P x *)
+ |> implies_intr ihyp
+ |> implies_intr (cprop_of x_D)
+ |> forall_intr (cterm_of thy x)
+
+ val subset_induct_rule =
+ acc_subset_induct
+ |> (curry op COMP) (assume D_subset)
+ |> (curry op COMP) (assume D_dcl)
+ |> (curry op COMP) (assume a_D)
+ |> (curry op COMP) istep
+ |> fold_rev implies_intr steps
+ |> implies_intr a_D
+ |> implies_intr D_dcl
+ |> implies_intr D_subset
+
+ val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
+
+ val simple_induct_rule =
+ subset_induct_rule
+ |> forall_intr (cterm_of thy D)
+ |> forall_elim (cterm_of thy acc_R)
+ |> assume_tac 1 |> Seq.hd
+ |> (curry op COMP) (acc_downward
+ |> (instantiate' [SOME (ctyp_of thy domT)]
+ (map (SOME o cterm_of thy) [R, x, z]))
+ |> forall_intr (cterm_of thy z)
+ |> forall_intr (cterm_of thy x))
+ |> forall_intr (cterm_of thy a)
+ |> forall_intr (cterm_of thy P)
+ in
+ simple_induct_rule
+ end
+
+
+
+(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
+fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
+ qglr = (oqs, _, _, _), ...} = clause
+ val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
+ |> fold_rev (curry Logic.mk_implies) gs
+ |> cterm_of thy
+ in
+ Goal.init goal
+ |> (SINGLE (resolve_tac [accI] 1)) |> the
+ |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
+ |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
+ |> Goal.conclude
+ |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+ end
+
+
+
+(** Termination rule **)
+
+val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule};
+val wf_in_rel = @{thm FunDef.wf_in_rel};
+val in_rel_def = @{thm FunDef.in_rel_def};
+
+fun mk_nest_term_case thy globals R' ihyp clause =
+ let
+ val Globals {x, z, ...} = globals
+ val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
+ qglr=(oqs, _, _, _), ...} = clause
+
+ val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
+
+ fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
+ let
+ val used = map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) (u @ sub)
+
+ val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
+ |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
+ |> Function_Ctx_Tree.export_term (fixes, assumes)
+ |> fold_rev (curry Logic.mk_implies o prop_of) ags
+ |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
+ |> cterm_of thy
+
+ val thm = assume hyp
+ |> fold forall_elim cqs
+ |> fold Thm.elim_implies ags
+ |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
+ |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *)
+
+ val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
+
+ val acc = thm COMP ih_case
+ val z_acc_local = acc
+ |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
+
+ val ethm = z_acc_local
+ |> Function_Ctx_Tree.export_thm thy (fixes,
+ z_eq_arg :: case_hyp :: ags @ assumes)
+ |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+
+ val sub' = sub @ [(([],[]), acc)]
+ in
+ (sub', (hyp :: hyps, ethm :: thms))
+ end
+ | step _ _ _ _ = raise Match
+ in
+ Function_Ctx_Tree.traverse_tree step tree
+ end
+
+
+fun mk_nest_term_rule thy globals R R_cases clauses =
+ let
+ val Globals { domT, x, z, ... } = globals
+ val acc_R = mk_acc domT R
+
+ val R' = Free ("R", fastype_of R)
+
+ val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
+ val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
+
+ val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
+
+ (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
+ val ihyp = Term.all domT $ Abs ("z", domT,
+ Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
+ HOLogic.mk_Trueprop (acc_R $ Bound 0)))
+ |> cterm_of thy
+
+ val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
+
+ val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
+
+ val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
+ in
+ R_cases
+ |> forall_elim (cterm_of thy z)
+ |> forall_elim (cterm_of thy x)
+ |> forall_elim (cterm_of thy (acc_R $ z))
+ |> curry op COMP (assume R_z_x)
+ |> fold_rev (curry op COMP) cases
+ |> implies_intr R_z_x
+ |> forall_intr (cterm_of thy z)
+ |> (fn it => it COMP accI)
+ |> implies_intr ihyp
+ |> forall_intr (cterm_of thy x)
+ |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
+ |> curry op RS (assume wfR')
+ |> forall_intr_vars
+ |> (fn it => it COMP allI)
+ |> fold implies_intr hyps
+ |> implies_intr wfR'
+ |> forall_intr (cterm_of thy R')
+ |> forall_elim (cterm_of thy (inrel_R))
+ |> curry op RS wf_in_rel
+ |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
+ |> forall_intr (cterm_of thy Rrel)
+ end
+
+
+
+(* Tail recursion (probably very fragile)
+ *
+ * FIXME:
+ * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
+ * - Must we really replace the fvar by f here?
+ * - Splitting is not configured automatically: Problems with case?
+ *)
+fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
+ let
+ val Globals {domT, ranT, fvar, ...} = globals
+
+ val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
+
+ val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *)
+ Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
+ (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
+ (fn {prems=[a], ...} =>
+ ((rtac (G_induct OF [a]))
+ THEN_ALL_NEW (rtac accI)
+ THEN_ALL_NEW (etac R_cases)
+ THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1)
+
+ val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
+
+ fun mk_trsimp clause psimp =
+ let
+ val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
+ val thy = ProofContext.theory_of ctxt
+ val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
+
+ val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
+ val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
+ fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
+ in
+ Goal.prove ctxt [] [] trsimp
+ (fn _ =>
+ rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
+ THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
+ THEN (simp_default_tac (simpset_of ctxt) 1)
+ THEN (etac not_acc_down 1)
+ THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
+ |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
+ end
+ in
+ map2 mk_trsimp clauses psimps
+ end
+
+
+fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
+ let
+ val FunctionConfig {domintros, tailrec, default=default_str, ...} = config
+
+ val fvar = Free (fname, fT)
+ val domT = domain_type fT
+ val ranT = range_type fT
+
+ val default = Syntax.parse_term lthy default_str
+ |> TypeInfer.constrain fT |> Syntax.check_term lthy
+
+ val (globals, ctxt') = fix_globals domT ranT fvar lthy
+
+ val Globals { x, h, ... } = globals
+
+ val clauses = map (mk_clause_context x ctxt') abstract_qglrs
+
+ val n = length abstract_qglrs
+
+ fun build_tree (ClauseContext { ctxt, rhs, ...}) =
+ Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
+
+ val trees = map build_tree clauses
+ val RCss = map find_calls trees
+
+ val ((G, GIntro_thms, G_elim, G_induct), 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 ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
+
+ val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
+ val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
+
+ val ((R, RIntro_thmss, R_elim), lthy) =
+ PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
+
+ val (_, lthy) =
+ LocalTheory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
+
+ val newthy = ProofContext.theory_of lthy
+ val clauses = map (transfer_clause_ctx newthy) clauses
+
+ val cert = cterm_of (ProofContext.theory_of lthy)
+
+ val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
+
+ val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
+ val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
+
+ val compat_store = store_compat_thms n compat
+
+ val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm
+
+ val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
+
+ fun mk_partial_rules provedgoal =
+ let
+ val newthy = theory_of_thm provedgoal (*FIXME*)
+
+ val (graph_is_function, complete_thm) =
+ provedgoal
+ |> Conjunction.elim
+ |> apfst (Thm.forall_elim_vars 0)
+
+ val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
+
+ val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
+
+ val simple_pinduct = PROFILE "Proving partial induction rule"
+ (mk_partial_induct_rule newthy globals R complete_thm) xclauses
+
+
+ val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
+
+ val dom_intros = if domintros
+ then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses)
+ else NONE
+ val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
+
+ in
+ FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
+ psimps=psimps, simple_pinducts=[simple_pinduct],
+ termination=total_intro, trsimps=trsimps,
+ domintros=dom_intros}
+ end
+ in
+ ((f, goalstate, mk_partial_rules), lthy)
+ end
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/function_lib.ML Sun Oct 25 00:10:25 2009 +0200
@@ -0,0 +1,180 @@
+(* Title: HOL/Tools/Function/fundef_lib.ML
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+Some fairly general functions that should probably go somewhere else...
+*)
+
+structure Function_Lib =
+struct
+
+fun map_option f NONE = NONE
+ | map_option f (SOME x) = SOME (f x);
+
+fun fold_option f NONE y = y
+ | fold_option f (SOME x) y = f x y;
+
+fun fold_map_option f NONE y = (NONE, y)
+ | fold_map_option f (SOME x) y = apfst SOME (f x y);
+
+(* Ex: "The variable" ^ plural " is" "s are" vs *)
+fun plural sg pl [x] = sg
+ | plural sg pl _ = pl
+
+(* lambda-abstracts over an arbitrarily nested tuple
+ ==> hologic.ML? *)
+fun tupled_lambda vars t =
+ case vars of
+ (Free v) => lambda (Free v) t
+ | (Var v) => lambda (Var v) t
+ | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
+ (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
+ | _ => raise Match
+
+
+fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
+ let
+ val (n, body) = Term.dest_abs a
+ in
+ (Free (n, T), body)
+ end
+ | dest_all _ = raise Match
+
+
+(* 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
+ in
+ (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)]
+ val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
+
+ val (n'', body) = Term.dest_abs (n', T, b)
+ val _ = (n' = n'') orelse error "dest_all_ctx"
+ (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
+
+ val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
+ in
+ (ctx'', (n', T) :: vs, bd)
+ end
+ | dest_all_all_ctx ctx t =
+ (ctx, [], t)
+
+
+fun map3 _ [] [] [] = []
+ | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
+ | map3 _ _ _ _ = raise Library.UnequalLengths;
+
+fun map4 _ [] [] [] [] = []
+ | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
+ | map4 _ _ _ _ _ = raise Library.UnequalLengths;
+
+fun map6 _ [] [] [] [] [] [] = []
+ | map6 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) = f x y z u v w :: map6 f xs ys zs us vs ws
+ | map6 _ _ _ _ _ _ _ = raise Library.UnequalLengths;
+
+fun map7 _ [] [] [] [] [] [] [] = []
+ | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
+ | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths;
+
+
+
+(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
+(* ==> library *)
+fun unordered_pairs [] = []
+ | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
+
+
+(* Replaces Frees by name. Works with loose Bounds. *)
+fun replace_frees assoc =
+ map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
+ | t => t)
+
+
+fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b))
+ | rename_bound n _ = raise Match
+
+fun mk_forall_rename (n, v) =
+ rename_bound n o Logic.all v
+
+fun forall_intr_rename (n, cv) thm =
+ let
+ val allthm = forall_intr cv thm
+ val (_ $ abs) = prop_of allthm
+ in
+ Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) 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
+
+
+datatype proof_attempt = Solved of thm | Stuck of thm | Fail
+
+fun try_proof cgoal tac =
+ case SINGLE tac (Goal.init cgoal) of
+ NONE => Fail
+ | SOME st =>
+ if Thm.no_prems st
+ then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st)
+ else Stuck st
+
+
+fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) =
+ if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
+ | dest_binop_list _ t = [ t ]
+
+
+(* separate two parts in a +-expression:
+ "a + b + c + d + e" --> "(a + b + d) + (c + e)"
+
+ Here, + can be any binary operation that is AC.
+
+ cn - The name of the binop-constructor (e.g. @{const_name Un})
+ ac - the AC rewrite rules for cn
+ is - the list of indices of the expressions that should become the first part
+ (e.g. [0,1,3] in the above example)
+*)
+
+fun regroup_conv neu cn ac is ct =
+ let
+ val mk = HOLogic.mk_binop cn
+ val t = term_of ct
+ val xs = dest_binop_list cn t
+ val js = subtract (op =) is (0 upto (length xs) - 1)
+ val ty = fastype_of t
+ val thy = theory_of_cterm ct
+ in
+ Goal.prove_internal []
+ (cterm_of thy
+ (Logic.mk_equals (t,
+ if is = []
+ then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
+ else if js = []
+ then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
+ else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
+ (K (rewrite_goals_tac ac
+ THEN rtac Drule.reflexive_thm 1))
+ end
+
+(* instance for unions *)
+fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
+ (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
+ @{thms Un_empty_right} @
+ @{thms Un_empty_left})) t
+
+
+end
--- a/src/HOL/Tools/Function/fundef.ML Sat Oct 24 20:27:26 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,226 +0,0 @@
-(* Title: HOL/Tools/Function/fundef.ML
- Author: Alexander Krauss, TU Muenchen
-
-A package for general recursive function definitions.
-Isar commands.
-*)
-
-signature FUNDEF =
-sig
- val add_fundef : (binding * typ option * mixfix) list
- -> (Attrib.binding * term) list
- -> FundefCommon.fundef_config
- -> local_theory
- -> Proof.state
- val add_fundef_cmd : (binding * string option * mixfix) list
- -> (Attrib.binding * string) list
- -> FundefCommon.fundef_config
- -> 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 : Proof.context -> thm list
-end
-
-
-structure Fundef : FUNDEF =
-struct
-
-open FundefLib
-open FundefCommon
-
-val simp_attribs = map (Attrib.internal o K)
- [Simplifier.simp_add,
- Code.add_default_eqn_attribute,
- Nitpick_Simps.add,
- Quickcheck_RecFun_Simps.add]
-
-val psimp_attribs = map (Attrib.internal o K)
- [Simplifier.simp_add,
- Nitpick_Psimps.add]
-
-fun note_theorem ((name, atts), ths) =
- LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
-
-fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
-
-fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
- let
- val spec = post simps
- |> map (apfst (apsnd (fn ats => moreatts @ ats)))
- |> map (apfst (apfst extra_qualify))
-
- val (saved_spec_simps, lthy) =
- fold_map (LocalTheory.note Thm.generatedK) spec lthy
-
- val saved_simps = maps snd saved_spec_simps
- val simps_by_f = sort saved_simps
-
- fun add_for_f fname simps =
- note_theorem ((Long_Name.qualify fname label, []), simps) #> snd
- in
- (saved_simps,
- fold2 add_for_f fnames simps_by_f lthy)
- end
-
-fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy =
- let
- val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
- val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
- val fixes = map (apfst (apfst Binding.name_of)) fixes0;
- val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
- val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config ctxt' fixes spec
-
- val defname = mk_defname fixes
-
- val ((goalstate, cont), lthy) =
- FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy
-
- fun afterqed [[proof]] lthy =
- let
- val FundefResult {fs, R, psimps, trsimps, simple_pinducts, termination,
- domintros, cases, ...} =
- cont (Thm.close_derivation proof)
-
- val fnames = map (fst o fst) fixes
- val qualify = Long_Name.qualify defname
- val addsmps = add_simps fnames post sort_cont
-
- val (((psimps', pinducts'), (_, [termination'])), lthy) =
- lthy
- |> addsmps (Binding.qualify false "partial") "psimps"
- psimp_attribs psimps
- ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
- ||>> note_theorem ((qualify "pinduct",
- [Attrib.internal (K (RuleCases.case_names cnames)),
- Attrib.internal (K (RuleCases.consumes 1)),
- Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
- ||>> note_theorem ((qualify "termination", []), [termination])
- ||> (snd o note_theorem ((qualify "cases",
- [Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
- ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
-
- val cdata = FundefCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
- pinducts=snd pinducts', termination=termination',
- fs=fs, R=R, defname=defname }
- val _ =
- if not is_external then ()
- else Specification.print_consts lthy (K false) (map fst fixes)
- in
- lthy
- |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata)
- end
- in
- lthy
- |> is_external ? LocalTheory.set_group (serial_string ())
- |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
- |> 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 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 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, add_simps, case_names, psimps,
- pinducts, defname, ...} = data
- val domT = domain_type (fastype_of R)
- val goal = HOLogic.mk_Trueprop
- (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
- fun afterqed [[totality]] lthy =
- let
- val totality = Thm.close_derivation totality
- val remove_domain_condition =
- full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
- val tsimps = map remove_domain_condition psimps
- val tinduct = map remove_domain_condition pinducts
- val qualify = Long_Name.qualify defname;
- in
- lthy
- |> add_simps I "simps" simp_attribs tsimps |> snd
- |> note_theorem
- ((qualify "induct",
- [Attrib.internal (K (RuleCases.case_names case_names))]),
- tinduct) |> snd
- end
- in
- lthy
- |> ProofContext.note_thmss ""
- [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
- |> ProofContext.note_thmss ""
- [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
- |> ProofContext.note_thmss ""
- [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
- [([Goal.norm_result termination], [])])] |> snd
- |> Proof.theorem_i NONE afterqed [[(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 ())
- |> termination_proof_cmd term_opt;
-
-
-(* Datatype hook to declare datatype congs as "fundef_congs" *)
-
-
-fun add_case_cong n thy =
- Context.theory_map (FundefCtxTree.map_fundef_congs (Thm.add_thm
- (Datatype.the_info thy n
- |> #case_cong
- |> safe_mk_meta_eq)))
- thy
-
-val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
-
-
-(* setup *)
-
-val setup =
- Attrib.setup @{binding fundef_cong}
- (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del)
- "declaration of congruence rule for function definitions"
- #> setup_case_cong
- #> FundefRelation.setup
- #> FundefCommon.Termination_Simps.setup
-
-val get_congs = FundefCtxTree.get_fundef_congs
-
-
-(* outer syntax *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ =
- OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
- (fundef_parser default_config
- >> (fn ((config, fixes), statements) => add_fundef_cmd fixes statements config));
-
-val _ =
- OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
- (Scan.option P.term >> termination_cmd);
-
-end;
-
-
-end
--- a/src/HOL/Tools/Function/fundef_common.ML Sat Oct 24 20:27:26 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,343 +0,0 @@
-(* Title: HOL/Tools/Function/fundef_common.ML
- Author: Alexander Krauss, TU Muenchen
-
-A package for general recursive function definitions.
-Common definitions and other infrastructure.
-*)
-
-structure FundefCommon =
-struct
-
-local open FundefLib in
-
-(* Profiling *)
-val profile = Unsynchronized.ref false;
-
-fun PROFILE msg = if !profile then timeap_msg msg else I
-
-
-val acc_const_name = @{const_name accp}
-fun mk_acc domT R =
- Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R
-
-val function_name = suffix "C"
-val graph_name = suffix "_graph"
-val rel_name = suffix "_rel"
-val dom_name = suffix "_dom"
-
-(* Termination rules *)
-
-structure TerminationRule = GenericDataFun
-(
- type T = thm list
- val empty = []
- val extend = I
- fun merge _ = Thm.merge_thms
-);
-
-val get_termination_rules = TerminationRule.get
-val store_termination_rule = TerminationRule.map o cons
-val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
-
-
-(* Function definition result data *)
-
-datatype fundef_result =
- FundefResult of
- {
- fs: term list,
- G: term,
- R: term,
-
- psimps : thm list,
- trsimps : thm list option,
-
- simple_pinducts : thm list,
- cases : thm,
- termination : thm,
- domintros : thm list option
- }
-
-
-datatype fundef_context_data =
- FundefCtxData of
- {
- defname : string,
-
- (* contains no logical entities: invariant under morphisms *)
- add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list
- -> local_theory -> thm list * local_theory,
- case_names : string list,
-
- fs : term list,
- R : term,
-
- psimps: thm list,
- pinducts: thm list,
- termination: thm
- }
-
-fun morph_fundef_data (FundefCtxData {add_simps, case_names, fs, R,
- psimps, pinducts, termination, defname}) phi =
- let
- val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
- val name = Binding.name_of o Morphism.binding phi o Binding.name
- in
- FundefCtxData { add_simps = add_simps, case_names = case_names,
- fs = map term fs, R = term R, psimps = fact psimps,
- pinducts = fact pinducts, termination = thm termination,
- defname = name defname }
- end
-
-structure FundefData = GenericDataFun
-(
- type T = (term * fundef_context_data) Item_Net.T;
- val empty = Item_Net.init
- (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
- fst;
- val copy = I;
- val extend = I;
- fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
-);
-
-val get_fundef = FundefData.get o Context.Proof;
-
-
-(* Generally useful?? *)
-fun lift_morphism thy f =
- let
- val term = Drule.term_rule thy f
- in
- Morphism.thm_morphism f $> Morphism.term_morphism term
- $> Morphism.typ_morphism (Logic.type_map term)
- end
-
-fun import_fundef_data t ctxt =
- let
- val thy = ProofContext.theory_of ctxt
- val ct = cterm_of thy t
- val inst_morph = lift_morphism thy o Thm.instantiate
-
- fun match (trm, data) =
- SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
- handle Pattern.MATCH => NONE
- in
- get_first match (Item_Net.retrieve (get_fundef ctxt) t)
- end
-
-fun import_last_fundef ctxt =
- case Item_Net.content (get_fundef ctxt) of
- [] => NONE
- | (t, data) :: _ =>
- let
- val ([t'], ctxt') = Variable.import_terms true [t] ctxt
- in
- import_fundef_data t' ctxt'
- end
-
-val all_fundef_data = Item_Net.content o get_fundef
-
-fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) =
- FundefData.map (fold (fn f => Item_Net.insert (f, data)) fs)
- #> store_termination_rule termination
-
-
-(* Simp rules for termination proofs *)
-
-structure Termination_Simps = Named_Thms
-(
- val name = "termination_simp"
- val description = "Simplification rule for termination proofs"
-);
-
-
-(* Default Termination Prover *)
-
-structure TerminationProver = GenericDataFun
-(
- type T = Proof.context -> Proof.method
- val empty = (fn _ => error "Termination prover not configured")
- val extend = I
- fun merge _ (a,b) = b (* FIXME *)
-);
-
-val set_termination_prover = TerminationProver.put
-val get_termination_prover = TerminationProver.get o Context.Proof
-
-
-(* Configuration management *)
-datatype fundef_opt
- = Sequential
- | Default of string
- | DomIntros
- | Tailrec
-
-datatype fundef_config
- = FundefConfig of
- {
- sequential: bool,
- default: string,
- domintros: bool,
- tailrec: bool
- }
-
-fun apply_opt Sequential (FundefConfig {sequential, default, domintros,tailrec}) =
- FundefConfig {sequential=true, default=default, domintros=domintros, tailrec=tailrec}
- | apply_opt (Default d) (FundefConfig {sequential, default, domintros,tailrec}) =
- FundefConfig {sequential=sequential, default=d, domintros=domintros, tailrec=tailrec}
- | apply_opt DomIntros (FundefConfig {sequential, default, domintros,tailrec}) =
- FundefConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec}
- | apply_opt Tailrec (FundefConfig {sequential, default, domintros,tailrec}) =
- FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
-
-val default_config =
- FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*),
- domintros=false, tailrec=false }
-
-
-(* Analyzing function equations *)
-
-fun split_def ctxt geq =
- let
- fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
- val qs = Term.strip_qnt_vars "all" geq
- val imp = Term.strip_qnt_body "all" geq
- val (gs, eq) = Logic.strip_horn imp
-
- val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
- handle TERM _ => error (input_error "Not an equation")
-
- val (head, args) = strip_comb f_args
-
- val fname = fst (dest_Free head)
- handle TERM _ => error (input_error "Head symbol must not be a bound variable")
- in
- (fname, qs, gs, args, rhs)
- end
-
-(* Check for all sorts of errors in the input *)
-fun check_defs ctxt fixes eqs =
- let
- val fnames = map (fst o fst) fixes
-
- fun check geq =
- let
- fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
-
- val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
-
- val _ = fname mem fnames
- orelse input_error
- ("Head symbol of left hand side must be "
- ^ plural "" "one out of " fnames ^ commas_quote fnames)
-
- val _ = length args > 0 orelse input_error "Function has no arguments:"
-
- fun add_bvs t is = add_loose_bnos (t, 0, is)
- val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
- |> map (fst o nth (rev qs))
-
- val _ = null rvs orelse input_error
- ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
- ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
-
- val _ = forall (not o Term.exists_subterm
- (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
- orelse input_error "Defined function may not occur in premises or arguments"
-
- val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
- val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
- val _ = null funvars
- orelse (warning (cat_lines
- ["Bound variable" ^ plural " " "s " funvars
- ^ commas_quote (map fst funvars) ^
- " occur" ^ plural "s" "" funvars ^ " in function position.",
- "Misspelled constructor???"]); true)
- in
- (fname, length args)
- end
-
- val _ = AList.group (op =) (map check eqs)
- |> map (fn (fname, ars) =>
- length (distinct (op =) ars) = 1
- orelse error ("Function " ^ quote fname ^
- " has different numbers of arguments in different equations"))
-
- fun check_sorts ((fname, fT), _) =
- Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
- orelse error (cat_lines
- ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
- setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
-
- val _ = map check_sorts fixes
- in
- ()
- end
-
-(* Preprocessors *)
-
-type fixes = ((string * typ) * mixfix) list
-type 'a spec = (Attrib.binding * 'a list) list
-type preproc = fundef_config -> Proof.context -> fixes -> term spec
- -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
-
-val fname_of = fst o dest_Free o fst o strip_comb o fst
- o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
-
-fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
- | mk_case_names _ n 0 = []
- | mk_case_names _ n 1 = [n]
- | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
-
-fun empty_preproc check _ ctxt fixes spec =
- let
- val (bnds, tss) = split_list spec
- val ts = flat tss
- val _ = check ctxt fixes ts
- val fnames = map (fst o fst) fixes
- val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
-
- fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1)
- (indices ~~ xs)
- |> map (map snd)
-
- (* using theorem names for case name currently disabled *)
- val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
- in
- (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
- end
-
-structure Preprocessor = GenericDataFun
-(
- type T = preproc
- val empty : T = empty_preproc check_defs
- val extend = I
- fun merge _ (a, _) = a
-);
-
-val get_preproc = Preprocessor.get o Context.Proof
-val set_preproc = Preprocessor.map o K
-
-
-
-local
- structure P = OuterParse and K = OuterKeyword
-
- val option_parser =
- P.group "option" ((P.reserved "sequential" >> K Sequential)
- || ((P.reserved "default" |-- P.term) >> Default)
- || (P.reserved "domintros" >> K DomIntros)
- || (P.reserved "tailrec" >> K Tailrec))
-
- fun config_parser default =
- (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
- >> (fn opts => fold apply_opt opts default)
-in
- fun fundef_parser default_cfg =
- config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
-end
-
-
-end
-end
-
--- a/src/HOL/Tools/Function/fundef_core.ML Sat Oct 24 20:27:26 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,956 +0,0 @@
-(* Title: HOL/Tools/Function/fundef_core.ML
- Author: Alexander Krauss, TU Muenchen
-
-A package for general recursive function definitions:
-Main functionality.
-*)
-
-signature FUNDEF_CORE =
-sig
- val trace: bool Unsynchronized.ref
-
- val prepare_fundef : FundefCommon.fundef_config
- -> string (* defname *)
- -> ((bstring * typ) * mixfix) list (* defined symbol *)
- -> ((bstring * typ) list * term list * term * term) list (* specification *)
- -> local_theory
-
- -> (term (* f *)
- * thm (* goalstate *)
- * (thm -> FundefCommon.fundef_result) (* continuation *)
- ) * local_theory
-
-end
-
-structure FundefCore : FUNDEF_CORE =
-struct
-
-val trace = Unsynchronized.ref false;
-fun trace_msg msg = if ! trace then tracing (msg ()) else ();
-
-val boolT = HOLogic.boolT
-val mk_eq = HOLogic.mk_eq
-
-open FundefLib
-open FundefCommon
-
-datatype globals =
- Globals of {
- fvar: term,
- domT: typ,
- ranT: typ,
- h: term,
- y: term,
- x: term,
- z: term,
- a: term,
- P: term,
- D: term,
- Pbool:term
-}
-
-
-datatype rec_call_info =
- RCInfo of
- {
- RIvs: (string * typ) list, (* Call context: fixes and assumes *)
- CCas: thm list,
- rcarg: term, (* The recursive argument *)
-
- llRI: thm,
- h_assum: term
- }
-
-
-datatype clause_context =
- ClauseContext of
- {
- ctxt : Proof.context,
-
- qs : term list,
- gs : term list,
- lhs: term,
- rhs: term,
-
- cqs: cterm list,
- ags: thm list,
- case_hyp : thm
- }
-
-
-fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
- ClauseContext { ctxt = ProofContext.transfer thy ctxt,
- qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
-
-
-datatype clause_info =
- ClauseInfo of
- {
- no: int,
- qglr : ((string * typ) list * term list * term * term),
- cdata : clause_context,
-
- tree: FundefCtxTree.ctx_tree,
- lGI: thm,
- RCs: rec_call_info list
- }
-
-
-(* Theory dependencies. *)
-val Pair_inject = @{thm Product_Type.Pair_inject};
-
-val acc_induct_rule = @{thm accp_induct_rule};
-
-val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
-val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness};
-val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff};
-
-val acc_downward = @{thm accp_downward};
-val accI = @{thm accp.accI};
-val case_split = @{thm HOL.case_split};
-val fundef_default_value = @{thm FunDef.fundef_default_value};
-val not_acc_down = @{thm not_accp_down};
-
-
-
-fun find_calls tree =
- let
- fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
- | add_Ri _ _ _ _ = raise Match
- in
- rev (FundefCtxTree.traverse_tree add_Ri tree [])
- end
-
-
-(** building proof obligations *)
-
-fun mk_compat_proof_obligations domT ranT fvar f glrs =
- let
- fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
- let
- val shift = incr_boundvars (length qs')
- in
- Logic.mk_implies
- (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
- HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
- |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
- |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
- |> curry abstract_over fvar
- |> curry subst_bound f
- end
- in
- map mk_impl (unordered_pairs glrs)
- end
-
-
-fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
- let
- fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
- HOLogic.mk_Trueprop Pbool
- |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
- |> fold_rev (curry Logic.mk_implies) gs
- |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
- in
- HOLogic.mk_Trueprop Pbool
- |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
- |> mk_forall_rename ("x", x)
- |> mk_forall_rename ("P", Pbool)
- end
-
-(** making a context with it's own local bindings **)
-
-fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
- let
- val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
- |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
-
- val thy = ProofContext.theory_of ctxt'
-
- fun inst t = subst_bounds (rev qs, t)
- val gs = map inst pre_gs
- val lhs = inst pre_lhs
- val rhs = inst pre_rhs
-
- val cqs = map (cterm_of thy) qs
- val ags = map (assume o cterm_of thy) gs
-
- val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
- in
- ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
- cqs = cqs, ags = ags, case_hyp = case_hyp }
- end
-
-
-(* lowlevel term function. FIXME: remove *)
-fun abstract_over_list vs body =
- let
- fun abs lev v tm =
- if v aconv tm then Bound lev
- else
- (case tm of
- Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
- | t $ u => abs lev v t $ abs lev v u
- | t => t);
- in
- fold_index (fn (i, v) => fn t => abs i v t) vs body
- end
-
-
-
-fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
- let
- val Globals {h, fvar, x, ...} = globals
-
- val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
- val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
-
- (* Instantiate the GIntro thm with "f" and import into the clause context. *)
- val lGI = GIntro_thm
- |> forall_elim (cert f)
- |> fold forall_elim cqs
- |> fold Thm.elim_implies ags
-
- fun mk_call_info (rcfix, rcassm, rcarg) RI =
- let
- val llRI = RI
- |> fold forall_elim cqs
- |> fold (forall_elim o cert o Free) rcfix
- |> fold Thm.elim_implies ags
- |> fold Thm.elim_implies rcassm
-
- val h_assum =
- HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
- |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
- |> fold_rev (Logic.all o Free) rcfix
- |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
- |> abstract_over_list (rev qs)
- in
- RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
- end
-
- val RC_infos = map2 mk_call_info RCs RIntro_thms
- in
- ClauseInfo
- {
- no=no,
- cdata=cdata,
- qglr=qglr,
-
- lGI=lGI,
- RCs=RC_infos,
- tree=tree
- }
- end
-
-
-
-
-
-
-
-(* replace this by a table later*)
-fun store_compat_thms 0 thms = []
- | store_compat_thms n thms =
- let
- val (thms1, thms2) = chop n thms
- in
- (thms1 :: store_compat_thms (n - 1) thms2)
- end
-
-(* expects i <= j *)
-fun lookup_compat_thm i j cts =
- nth (nth cts (i - 1)) (j - i)
-
-(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
-(* 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 (HOLogic.mk_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" *)
- |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
- |> fold Thm.elim_implies agsj
- |> fold Thm.elim_implies agsi
- |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
- end
- else
- 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 Thm.elim_implies agsi
- |> fold Thm.elim_implies agsj
- |> Thm.elim_implies (assume lhsi_eq_lhsj)
- |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
- end
- end
-
-
-
-
-(* Generates the replacement lemma in fully quantified form. *)
-fun mk_replacement_lemma thy h ih_elim clause =
- let
- val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
- local open Conv in
- val ih_conv = arg1_conv o arg_conv o arg_conv
- end
-
- val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
-
- val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
- val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
-
- val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
-
- val replace_lemma = (eql RS meta_eq_to_obj_eq)
- |> implies_intr (cprop_of case_hyp)
- |> fold_rev (implies_intr o cprop_of) h_assums
- |> fold_rev (implies_intr o cprop_of) ags
- |> fold_rev forall_intr cqs
- |> Thm.close_derivation
- in
- replace_lemma
- end
-
-
-fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
- let
- val Globals {h, y, x, fvar, ...} = globals
- val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
- val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
-
- val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
- = mk_clause_context x ctxti cdescj
-
- val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
- val compat = get_compat_thm thy compat_store i j cctxi cctxj
- val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
-
- val RLj_import =
- RLj |> fold forall_elim cqsj'
- |> fold Thm.elim_implies agsj'
- |> fold Thm.elim_implies Ghsj'
-
- val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
- val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
- in
- (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
- |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
- |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
- |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
- |> fold_rev (implies_intr o cprop_of) Ghsj'
- |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
- |> implies_intr (cprop_of y_eq_rhsj'h)
- |> implies_intr (cprop_of lhsi_eq_lhsj')
- |> fold_rev forall_intr (cterm_of thy h :: cqsj')
- end
-
-
-
-fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
- let
- val Globals {x, y, ranT, fvar, ...} = globals
- val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
- val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
-
- val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
-
- fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
- |> fold_rev (implies_intr o cprop_of) CCas
- |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
-
- val existence = fold (curry op COMP o prep_RC) RCs lGI
-
- val P = cterm_of thy (mk_eq (y, rhsC))
- val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
-
- val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
-
- val uniqueness = G_cases
- |> forall_elim (cterm_of thy lhs)
- |> forall_elim (cterm_of thy y)
- |> forall_elim P
- |> Thm.elim_implies G_lhs_y
- |> fold Thm.elim_implies unique_clauses
- |> implies_intr (cprop_of G_lhs_y)
- |> forall_intr (cterm_of thy y)
-
- val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
-
- val exactly_one =
- ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
- |> curry (op COMP) existence
- |> curry (op COMP) uniqueness
- |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
- |> implies_intr (cprop_of case_hyp)
- |> fold_rev (implies_intr o cprop_of) ags
- |> fold_rev forall_intr cqs
-
- val function_value =
- existence
- |> implies_intr ihyp
- |> implies_intr (cprop_of case_hyp)
- |> forall_intr (cterm_of thy x)
- |> forall_elim (cterm_of thy lhs)
- |> curry (op RS) refl
- in
- (exactly_one, function_value)
- end
-
-
-
-
-fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
- let
- val Globals {h, domT, ranT, x, ...} = globals
- val thy = ProofContext.theory_of ctxt
-
- (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
- val ihyp = Term.all domT $ Abs ("z", domT,
- Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
- HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
- Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
- |> cterm_of thy
-
- val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
- val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
- val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
- |> instantiate' [] [NONE, SOME (cterm_of thy h)]
-
- val _ = trace_msg (K "Proving Replacement lemmas...")
- val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
-
- val _ = trace_msg (K "Proving cases for unique existence...")
- val (ex1s, values) =
- split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
-
- val _ = trace_msg (K "Proving: Graph is a function")
- val graph_is_function = complete
- |> Thm.forall_elim_vars 0
- |> fold (curry op COMP) ex1s
- |> implies_intr (ihyp)
- |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
- |> 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 o Var) (Term.add_vars (prop_of it) []) it)
-
- val goalstate = Conjunction.intr graph_is_function complete
- |> Thm.close_derivation
- |> Goal.protect
- |> fold_rev (implies_intr o cprop_of) compat
- |> implies_intr (cprop_of complete)
- in
- (goalstate, values)
- end
-
-
-fun define_graph Gname fvar domT ranT clauses RCss lthy =
- let
- val GT = domT --> ranT --> boolT
- val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
-
- fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
- let
- fun mk_h_assm (rcfix, rcassm, rcarg) =
- HOLogic.mk_Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
- |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
- |> fold_rev (Logic.all o Free) rcfix
- in
- HOLogic.mk_Trueprop (Gvar $ lhs $ rhs)
- |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
- |> fold_rev (curry Logic.mk_implies) gs
- |> fold_rev Logic.all (fvar :: qs)
- end
-
- val G_intros = map2 mk_GIntro clauses RCss
-
- val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
- FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
- in
- ((G, GIntro_thms, G_elim, G_induct), lthy)
- end
-
-
-
-fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
- let
- val f_def =
- Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
- Abs ("y", ranT, G $ Bound 1 $ Bound 0))
- |> Syntax.check_term lthy
-
- val ((f, (_, f_defthm)), lthy) =
- LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy
- in
- ((f, f_defthm), lthy)
- end
-
-
-fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
- let
-
- val RT = domT --> domT --> boolT
- val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
-
- fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
- HOLogic.mk_Trueprop (Rvar $ rcarg $ lhs)
- |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
- |> fold_rev (curry Logic.mk_implies) gs
- |> fold_rev (Logic.all o Free) rcfix
- |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
- (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
-
- val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
-
- val (RIntro_thmss, (R, R_elim, _, lthy)) =
- fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
- in
- ((R, RIntro_thmss, R_elim), lthy)
- end
-
-
-fun fix_globals domT ranT fvar ctxt =
- let
- val ([h, y, x, z, a, D, P, Pbool],ctxt') =
- Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
- in
- (Globals {h = Free (h, domT --> ranT),
- y = Free (y, ranT),
- x = Free (x, domT),
- z = Free (z, domT),
- a = Free (a, domT),
- D = Free (D, domT --> boolT),
- P = Free (P, domT --> boolT),
- Pbool = Free (Pbool, boolT),
- fvar = fvar,
- domT = domT,
- ranT = ranT
- },
- ctxt')
- end
-
-
-
-fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
- let
- fun inst_term t = subst_bound(f, abstract_over (fvar, t))
- in
- (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
- end
-
-
-
-(**********************************************************
- * PROVING THE RULES
- **********************************************************)
-
-fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
- let
- val Globals {domT, z, ...} = globals
-
- fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
- let
- val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
- val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
- in
- ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
- |> (fn it => it COMP graph_is_function)
- |> implies_intr z_smaller
- |> forall_intr (cterm_of thy z)
- |> (fn it => it COMP valthm)
- |> implies_intr lhs_acc
- |> asm_simplify (HOL_basic_ss addsimps [f_iff])
- |> fold_rev (implies_intr o cprop_of) ags
- |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
- end
- in
- map2 mk_psimp clauses valthms
- end
-
-
-(** Induction rule **)
-
-
-val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
-
-
-fun mk_partial_induct_rule thy globals R complete_thm clauses =
- let
- val Globals {domT, x, z, a, P, D, ...} = globals
- val acc_R = mk_acc domT R
-
- val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
- val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
-
- val D_subset = cterm_of thy (Logic.all x
- (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
-
- val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
- Logic.all x
- (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
- Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
- HOLogic.mk_Trueprop (D $ z)))))
- |> cterm_of thy
-
-
- (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
- val ihyp = Term.all domT $ Abs ("z", domT,
- Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
- HOLogic.mk_Trueprop (P $ Bound 0)))
- |> cterm_of thy
-
- val aihyp = assume ihyp
-
- fun prove_case clause =
- let
- val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
- qglr = (oqs, _, _, _), ...} = clause
-
- val case_hyp_conv = K (case_hyp RS eq_reflection)
- local open Conv in
- val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
- val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
- end
-
- fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
- sih |> forall_elim (cterm_of thy rcarg)
- |> Thm.elim_implies llRI
- |> fold_rev (implies_intr o cprop_of) CCas
- |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
-
- val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
-
- val step = HOLogic.mk_Trueprop (P $ lhs)
- |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
- |> fold_rev (curry Logic.mk_implies) gs
- |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
- |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
- |> cterm_of thy
-
- val P_lhs = assume step
- |> fold forall_elim cqs
- |> Thm.elim_implies lhs_D
- |> fold Thm.elim_implies ags
- |> fold Thm.elim_implies P_recs
-
- val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
- |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
- |> symmetric (* P lhs == P x *)
- |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
- |> implies_intr (cprop_of case_hyp)
- |> fold_rev (implies_intr o cprop_of) ags
- |> fold_rev forall_intr cqs
- in
- (res, step)
- end
-
- val (cases, steps) = split_list (map prove_case clauses)
-
- val istep = complete_thm
- |> Thm.forall_elim_vars 0
- |> fold (curry op COMP) cases (* P x *)
- |> implies_intr ihyp
- |> implies_intr (cprop_of x_D)
- |> forall_intr (cterm_of thy x)
-
- val subset_induct_rule =
- acc_subset_induct
- |> (curry op COMP) (assume D_subset)
- |> (curry op COMP) (assume D_dcl)
- |> (curry op COMP) (assume a_D)
- |> (curry op COMP) istep
- |> fold_rev implies_intr steps
- |> implies_intr a_D
- |> implies_intr D_dcl
- |> implies_intr D_subset
-
- val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
-
- val simple_induct_rule =
- subset_induct_rule
- |> forall_intr (cterm_of thy D)
- |> forall_elim (cterm_of thy acc_R)
- |> assume_tac 1 |> Seq.hd
- |> (curry op COMP) (acc_downward
- |> (instantiate' [SOME (ctyp_of thy domT)]
- (map (SOME o cterm_of thy) [R, x, z]))
- |> forall_intr (cterm_of thy z)
- |> forall_intr (cterm_of thy x))
- |> forall_intr (cterm_of thy a)
- |> forall_intr (cterm_of thy P)
- in
- simple_induct_rule
- end
-
-
-
-(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
-fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
- let
- val thy = ProofContext.theory_of ctxt
- val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
- qglr = (oqs, _, _, _), ...} = clause
- val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
- |> fold_rev (curry Logic.mk_implies) gs
- |> cterm_of thy
- in
- Goal.init goal
- |> (SINGLE (resolve_tac [accI] 1)) |> the
- |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
- |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
- |> Goal.conclude
- |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
- end
-
-
-
-(** Termination rule **)
-
-val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule};
-val wf_in_rel = @{thm FunDef.wf_in_rel};
-val in_rel_def = @{thm FunDef.in_rel_def};
-
-fun mk_nest_term_case thy globals R' ihyp clause =
- let
- val Globals {x, z, ...} = globals
- val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
- qglr=(oqs, _, _, _), ...} = clause
-
- val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
-
- fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
- let
- val used = map (fn (ctx,thm) => FundefCtxTree.export_thm thy ctx thm) (u @ sub)
-
- val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
- |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
- |> FundefCtxTree.export_term (fixes, assumes)
- |> fold_rev (curry Logic.mk_implies o prop_of) ags
- |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
- |> cterm_of thy
-
- val thm = assume hyp
- |> fold forall_elim cqs
- |> fold Thm.elim_implies ags
- |> FundefCtxTree.import_thm thy (fixes, assumes)
- |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *)
-
- val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
-
- val acc = thm COMP ih_case
- val z_acc_local = acc
- |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
-
- val ethm = z_acc_local
- |> FundefCtxTree.export_thm thy (fixes,
- z_eq_arg :: case_hyp :: ags @ assumes)
- |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
-
- val sub' = sub @ [(([],[]), acc)]
- in
- (sub', (hyp :: hyps, ethm :: thms))
- end
- | step _ _ _ _ = raise Match
- in
- FundefCtxTree.traverse_tree step tree
- end
-
-
-fun mk_nest_term_rule thy globals R R_cases clauses =
- let
- val Globals { domT, x, z, ... } = globals
- val acc_R = mk_acc domT R
-
- val R' = Free ("R", fastype_of R)
-
- val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
- val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
-
- val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
-
- (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
- val ihyp = Term.all domT $ Abs ("z", domT,
- Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
- HOLogic.mk_Trueprop (acc_R $ Bound 0)))
- |> cterm_of thy
-
- val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
-
- val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
-
- val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
- in
- R_cases
- |> forall_elim (cterm_of thy z)
- |> forall_elim (cterm_of thy x)
- |> forall_elim (cterm_of thy (acc_R $ z))
- |> curry op COMP (assume R_z_x)
- |> fold_rev (curry op COMP) cases
- |> implies_intr R_z_x
- |> forall_intr (cterm_of thy z)
- |> (fn it => it COMP accI)
- |> implies_intr ihyp
- |> forall_intr (cterm_of thy x)
- |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
- |> curry op RS (assume wfR')
- |> forall_intr_vars
- |> (fn it => it COMP allI)
- |> fold implies_intr hyps
- |> implies_intr wfR'
- |> forall_intr (cterm_of thy R')
- |> forall_elim (cterm_of thy (inrel_R))
- |> curry op RS wf_in_rel
- |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
- |> forall_intr (cterm_of thy Rrel)
- end
-
-
-
-(* Tail recursion (probably very fragile)
- *
- * FIXME:
- * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
- * - Must we really replace the fvar by f here?
- * - Splitting is not configured automatically: Problems with case?
- *)
-fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
- let
- val Globals {domT, ranT, fvar, ...} = globals
-
- val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
-
- val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *)
- Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
- (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
- (fn {prems=[a], ...} =>
- ((rtac (G_induct OF [a]))
- THEN_ALL_NEW (rtac accI)
- THEN_ALL_NEW (etac R_cases)
- THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1)
-
- val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
-
- fun mk_trsimp clause psimp =
- let
- val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
- val thy = ProofContext.theory_of ctxt
- val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
-
- val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
- val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
- fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
- in
- Goal.prove ctxt [] [] trsimp
- (fn _ =>
- rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
- THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
- THEN (simp_default_tac (simpset_of ctxt) 1)
- THEN (etac not_acc_down 1)
- THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
- |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
- end
- in
- map2 mk_trsimp clauses psimps
- end
-
-
-fun prepare_fundef config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
- let
- val FundefConfig {domintros, tailrec, default=default_str, ...} = config
-
- val fvar = Free (fname, fT)
- val domT = domain_type fT
- val ranT = range_type fT
-
- val default = Syntax.parse_term lthy default_str
- |> TypeInfer.constrain fT |> Syntax.check_term lthy
-
- val (globals, ctxt') = fix_globals domT ranT fvar lthy
-
- val Globals { x, h, ... } = globals
-
- val clauses = map (mk_clause_context x ctxt') abstract_qglrs
-
- val n = length abstract_qglrs
-
- fun build_tree (ClauseContext { ctxt, rhs, ...}) =
- FundefCtxTree.mk_tree (fname, fT) h ctxt rhs
-
- val trees = map build_tree clauses
- val RCss = map find_calls trees
-
- val ((G, GIntro_thms, G_elim, G_induct), 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 ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
-
- val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
- val 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 (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
-
- val (_, lthy) =
- LocalTheory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
-
- val newthy = ProofContext.theory_of lthy
- val clauses = map (transfer_clause_ctx newthy) clauses
-
- val cert = cterm_of (ProofContext.theory_of lthy)
-
- val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
-
- val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
- val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
-
- val compat_store = store_compat_thms n compat
-
- val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm
-
- val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
-
- fun mk_partial_rules provedgoal =
- let
- val newthy = theory_of_thm provedgoal (*FIXME*)
-
- val (graph_is_function, complete_thm) =
- provedgoal
- |> Conjunction.elim
- |> apfst (Thm.forall_elim_vars 0)
-
- val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
-
- val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
-
- val simple_pinduct = PROFILE "Proving partial induction rule"
- (mk_partial_induct_rule newthy globals R complete_thm) xclauses
-
-
- val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
-
- val dom_intros = if domintros
- then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses)
- else NONE
- val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
-
- in
- FundefResult {fs=[f], G=G, R=R, cases=complete_thm,
- psimps=psimps, simple_pinducts=[simple_pinduct],
- termination=total_intro, trsimps=trsimps,
- domintros=dom_intros}
- end
- in
- ((f, goalstate, mk_partial_rules), lthy)
- end
-
-
-end
--- a/src/HOL/Tools/Function/fundef_datatype.ML Sat Oct 24 20:27:26 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,178 +0,0 @@
-(* Title: HOL/Tools/Function/fundef_datatype.ML
- Author: Alexander Krauss, TU Muenchen
-
-A package for general recursive function definitions.
-A tactic to prove completeness of datatype patterns.
-*)
-
-signature FUNDEF_DATATYPE =
-sig
- val add_fun : FundefCommon.fundef_config ->
- (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
- bool -> local_theory -> Proof.context
- val add_fun_cmd : FundefCommon.fundef_config ->
- (binding * string option * mixfix) list -> (Attrib.binding * string) list ->
- bool -> local_theory -> Proof.context
-
- val setup : theory -> theory
-end
-
-structure FundefDatatype : FUNDEF_DATATYPE =
-struct
-
-open FundefLib
-open FundefCommon
-
-
-fun check_pats ctxt geq =
- let
- fun err str = error (cat_lines ["Malformed definition:",
- str ^ " not allowed in sequential mode.",
- Syntax.string_of_term ctxt geq])
- val thy = ProofContext.theory_of ctxt
-
- fun check_constr_pattern (Bound _) = ()
- | check_constr_pattern t =
- let
- val (hd, args) = strip_comb t
- in
- (((case Datatype.info_of_constr thy (dest_Const hd) of
- SOME _ => ()
- | NONE => err "Non-constructor pattern")
- handle TERM ("dest_Const", _) => err "Non-constructor patterns");
- map check_constr_pattern args;
- ())
- end
-
- val (fname, qs, gs, args, rhs) = split_def ctxt geq
-
- val _ = if not (null gs) then err "Conditional equations" else ()
- val _ = map check_constr_pattern args
-
- (* just count occurrences to check linearity *)
- val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs
- then err "Nonlinear patterns" else ()
- in
- ()
- end
-
-val by_pat_completeness_auto =
- Proof.global_future_terminal_proof
- (Method.Basic Pat_Completeness.pat_completeness,
- SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
-
-fun termination_by method int =
- Fundef.termination_proof NONE
- #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
-
-fun mk_catchall fixes arity_of =
- let
- fun mk_eqn ((fname, fT), _) =
- let
- val n = arity_of fname
- val (argTs, rT) = chop n (binder_types fT)
- |> apsnd (fn Ts => Ts ---> body_type fT)
-
- val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
- in
- HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
- Const ("HOL.undefined", rT))
- |> HOLogic.mk_Trueprop
- |> fold_rev Logic.all qs
- end
- in
- map mk_eqn fixes
- end
-
-fun add_catchall ctxt fixes spec =
- let val fqgars = map (split_def ctxt) spec
- val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
- |> AList.lookup (op =) #> the
- in
- spec @ mk_catchall fixes arity_of
- end
-
-fun warn_if_redundant ctxt origs tss =
- let
- fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
-
- val (tss', _) = chop (length origs) tss
- fun check (t, []) = (warning (msg t); [])
- | check (t, s) = s
- in
- (map check (origs ~~ tss'); tss)
- end
-
-
-fun sequential_preproc (config as FundefConfig {sequential, ...}) ctxt fixes spec =
- if sequential then
- let
- val (bnds, eqss) = split_list spec
-
- val eqs = map the_single eqss
-
- val feqs = eqs
- |> tap (check_defs ctxt fixes) (* Standard checks *)
- |> tap (map (check_pats ctxt)) (* More checks for sequential mode *)
-
- val compleqs = add_catchall ctxt fixes feqs (* Completion *)
-
- val spliteqs = warn_if_redundant ctxt feqs
- (FundefSplit.split_all_equations ctxt compleqs)
-
- fun restore_spec thms =
- bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms)
-
- val spliteqs' = flat (Library.take (length bnds, spliteqs))
- val fnames = map (fst o fst) fixes
- val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
-
- fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
- |> map (map snd)
-
-
- val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding
-
- (* using theorem names for case name currently disabled *)
- val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es))
- (bnds' ~~ spliteqs)
- |> flat
- in
- (flat spliteqs, restore_spec, sort, case_names)
- end
- else
- FundefCommon.empty_preproc check_defs config ctxt fixes spec
-
-val setup =
- Context.theory_map (FundefCommon.set_preproc sequential_preproc)
-
-
-val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*),
- domintros=false, tailrec=false }
-
-fun gen_fun add config fixes statements int lthy =
- let val group = serial_string () in
- lthy
- |> LocalTheory.set_group group
- |> add fixes statements config
- |> by_pat_completeness_auto int
- |> LocalTheory.restore
- |> LocalTheory.set_group group
- |> termination_by (FundefCommon.get_termination_prover lthy) int
- end;
-
-val add_fun = gen_fun Fundef.add_fundef
-val add_fun_cmd = gen_fun Fundef.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), statements) => add_fun_cmd config fixes statements));
-
-end
-
-end
--- a/src/HOL/Tools/Function/fundef_lib.ML Sat Oct 24 20:27:26 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,179 +0,0 @@
-(* Title: HOL/Tools/Function/fundef_lib.ML
- Author: Alexander Krauss, TU Muenchen
-
-A package for general recursive function definitions.
-Some fairly general functions that should probably go somewhere else...
-*)
-
-structure FundefLib = struct
-
-fun map_option f NONE = NONE
- | map_option f (SOME x) = SOME (f x);
-
-fun fold_option f NONE y = y
- | fold_option f (SOME x) y = f x y;
-
-fun fold_map_option f NONE y = (NONE, y)
- | fold_map_option f (SOME x) y = apfst SOME (f x y);
-
-(* Ex: "The variable" ^ plural " is" "s are" vs *)
-fun plural sg pl [x] = sg
- | plural sg pl _ = pl
-
-(* lambda-abstracts over an arbitrarily nested tuple
- ==> hologic.ML? *)
-fun tupled_lambda vars t =
- case vars of
- (Free v) => lambda (Free v) t
- | (Var v) => lambda (Var v) t
- | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
- (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
- | _ => raise Match
-
-
-fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
- let
- val (n, body) = Term.dest_abs a
- in
- (Free (n, T), body)
- end
- | dest_all _ = raise Match
-
-
-(* 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
- in
- (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)]
- val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
-
- val (n'', body) = Term.dest_abs (n', T, b)
- val _ = (n' = n'') orelse error "dest_all_ctx"
- (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
-
- val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
- in
- (ctx'', (n', T) :: vs, bd)
- end
- | dest_all_all_ctx ctx t =
- (ctx, [], t)
-
-
-fun map3 _ [] [] [] = []
- | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
- | map3 _ _ _ _ = raise Library.UnequalLengths;
-
-fun map4 _ [] [] [] [] = []
- | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
- | map4 _ _ _ _ _ = raise Library.UnequalLengths;
-
-fun map6 _ [] [] [] [] [] [] = []
- | map6 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) = f x y z u v w :: map6 f xs ys zs us vs ws
- | map6 _ _ _ _ _ _ _ = raise Library.UnequalLengths;
-
-fun map7 _ [] [] [] [] [] [] [] = []
- | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
- | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths;
-
-
-
-(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
-(* ==> library *)
-fun unordered_pairs [] = []
- | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
-
-
-(* Replaces Frees by name. Works with loose Bounds. *)
-fun replace_frees assoc =
- map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
- | t => t)
-
-
-fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b))
- | rename_bound n _ = raise Match
-
-fun mk_forall_rename (n, v) =
- rename_bound n o Logic.all v
-
-fun forall_intr_rename (n, cv) thm =
- let
- val allthm = forall_intr cv thm
- val (_ $ abs) = prop_of allthm
- in
- Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) 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
-
-
-datatype proof_attempt = Solved of thm | Stuck of thm | Fail
-
-fun try_proof cgoal tac =
- case SINGLE tac (Goal.init cgoal) of
- NONE => Fail
- | SOME st =>
- if Thm.no_prems st
- then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st)
- else Stuck st
-
-
-fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) =
- if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
- | dest_binop_list _ t = [ t ]
-
-
-(* separate two parts in a +-expression:
- "a + b + c + d + e" --> "(a + b + d) + (c + e)"
-
- Here, + can be any binary operation that is AC.
-
- cn - The name of the binop-constructor (e.g. @{const_name Un})
- ac - the AC rewrite rules for cn
- is - the list of indices of the expressions that should become the first part
- (e.g. [0,1,3] in the above example)
-*)
-
-fun regroup_conv neu cn ac is ct =
- let
- val mk = HOLogic.mk_binop cn
- val t = term_of ct
- val xs = dest_binop_list cn t
- val js = subtract (op =) is (0 upto (length xs) - 1)
- val ty = fastype_of t
- val thy = theory_of_cterm ct
- in
- Goal.prove_internal []
- (cterm_of thy
- (Logic.mk_equals (t,
- if is = []
- then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
- else if js = []
- then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
- else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
- (K (rewrite_goals_tac ac
- THEN rtac Drule.reflexive_thm 1))
- end
-
-(* instance for unions *)
-fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
- (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
- @{thms Un_empty_right} @
- @{thms Un_empty_left})) t
-
-
-end
--- a/src/HOL/Tools/Function/induction_scheme.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/Function/induction_scheme.ML Sun Oct 25 00:10:25 2009 +0200
@@ -13,10 +13,10 @@
end
-structure InductionScheme : INDUCTION_SCHEME =
+structure Induction_Scheme : INDUCTION_SCHEME =
struct
-open FundefLib
+open Function_Lib
type rec_call_info = int * (string * typ) list * term list * term list
--- a/src/HOL/Tools/Function/inductive_wrap.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/Function/inductive_wrap.ML Sun Oct 25 00:10:25 2009 +0200
@@ -6,17 +6,17 @@
the introduction and elimination rules.
*)
-signature FUNDEF_INDUCTIVE_WRAP =
+signature FUNCTION_INDUCTIVE_WRAP =
sig
val inductive_def : term list
-> ((bstring * typ) * mixfix) * local_theory
-> thm list * (term * thm * thm * local_theory)
end
-structure FundefInductiveWrap: FUNDEF_INDUCTIVE_WRAP =
+structure Function_Inductive_Wrap: FUNCTION_INDUCTIVE_WRAP =
struct
-open FundefLib
+open Function_Lib
fun requantify ctxt lfix orig_def thm =
let
--- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Sun Oct 25 00:10:25 2009 +0200
@@ -13,10 +13,10 @@
val setup: theory -> theory
end
-structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
+structure Lexicographic_Order : LEXICOGRAPHIC_ORDER =
struct
-open FundefLib
+open Function_Lib
(** General stuff **)
@@ -58,7 +58,7 @@
fun dest_term (t : term) =
let
- val (vars, prop) = FundefLib.dest_all_all t
+ val (vars, prop) = Function_Lib.dest_all_all t
val (prems, concl) = Logic.strip_horn prop
val (lhs, rhs) = concl
|> HOLogic.dest_Trueprop
@@ -215,9 +215,9 @@
end
fun lexicographic_order_tac ctxt =
- TRY (FundefCommon.apply_termination_rule ctxt 1)
+ TRY (Function_Common.apply_termination_rule ctxt 1)
THEN lex_order_tac ctxt
- (auto_tac (clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
+ (auto_tac (clasimpset_of ctxt addsimps2 Function_Common.Termination_Simps.get ctxt))
val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
@@ -225,7 +225,7 @@
Method.setup @{binding lexicographic_order}
(Method.sections clasimp_modifiers >> (K lexicographic_order))
"termination prover for lexicographic orderings"
- #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order)
+ #> Context.theory_map (Function_Common.set_termination_prover lexicographic_order)
end;
--- a/src/HOL/Tools/Function/mutual.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Sun Oct 25 00:10:25 2009 +0200
@@ -5,29 +5,26 @@
Tools for mutual recursive definitions.
*)
-signature FUNDEF_MUTUAL =
+signature FUNCTION_MUTUAL =
sig
- val prepare_fundef_mutual : FundefCommon.fundef_config
+ val prepare_function_mutual : Function_Common.function_config
-> string (* defname *)
-> ((string * typ) * mixfix) list
-> term list
-> local_theory
-> ((thm (* goalstate *)
- * (thm -> FundefCommon.fundef_result) (* proof continuation *)
+ * (thm -> Function_Common.function_result) (* proof continuation *)
) * local_theory)
end
-structure FundefMutual: FUNDEF_MUTUAL =
+structure Function_Mutual: FUNCTION_MUTUAL =
struct
-open FundefLib
-open FundefCommon
-
-
-
+open Function_Lib
+open Function_Common
type qgar = string * (string * typ) list * term list * term list * term
@@ -268,7 +265,7 @@
fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
let
val result = inner_cont proof
- val FundefResult {fs=[f], G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
+ val FunctionResult {fs=[f], G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
termination,domintros} = result
val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
@@ -288,20 +285,20 @@
val mtermination = full_simplify rew_ss termination
val mdomintros = map_option (map (full_simplify rew_ss)) domintros
in
- FundefResult { fs=fs, G=G, R=R,
+ FunctionResult { fs=fs, G=G, R=R,
psimps=mpsimps, simple_pinducts=minducts,
cases=cases, termination=mtermination,
domintros=mdomintros,
trsimps=mtrsimps}
end
-fun prepare_fundef_mutual config defname fixes eqss lthy =
+fun prepare_function_mutual config defname fixes eqss lthy =
let
val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
val Mutual {fsum_var=(n, T), qglrs, ...} = mutual
val ((fsum, goalstate, cont), lthy') =
- FundefCore.prepare_fundef config defname [((n, T), NoSyn)] qglrs lthy
+ Function_Core.prepare_function config defname [((n, T), NoSyn)] qglrs lthy
val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
--- a/src/HOL/Tools/Function/pat_completeness.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/Function/pat_completeness.ML Sun Oct 25 00:10:25 2009 +0200
@@ -17,8 +17,8 @@
structure Pat_Completeness : PAT_COMPLETENESS =
struct
-open FundefLib
-open FundefCommon
+open Function_Lib
+open Function_Common
fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
--- a/src/HOL/Tools/Function/pattern_split.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/Function/pattern_split.ML Sun Oct 25 00:10:25 2009 +0200
@@ -8,7 +8,7 @@
*)
-signature FUNDEF_SPLIT =
+signature FUNCTION_SPLIT =
sig
val split_some_equations :
Proof.context -> (bool * term) list -> term list list
@@ -17,10 +17,10 @@
Proof.context -> term list -> term list list
end
-structure FundefSplit : FUNDEF_SPLIT =
+structure Function_Split : FUNCTION_SPLIT =
struct
-open FundefLib
+open Function_Lib
(* We use proof context for the variable management *)
(* FIXME: no __ *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/relation.ML Sun Oct 25 00:10:25 2009 +0200
@@ -0,0 +1,36 @@
+(* Title: HOL/Tools/Function/relation.ML
+ Author: Alexander Krauss, TU Muenchen
+
+A package for general recursive function definitions.
+Method "relation" to commence a termination proof using a user-specified relation.
+*)
+
+signature FUNCTION_RELATION =
+sig
+ val relation_tac: Proof.context -> term -> int -> tactic
+ val setup: theory -> theory
+end
+
+structure Function_Relation : FUNCTION_RELATION =
+struct
+
+fun inst_thm ctxt rel st =
+ let
+ val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+ val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
+ val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
+ val Rvar = cert (Var (the_single (Term.add_vars (prop_of st') [])))
+ in
+ Drule.cterm_instantiate [(Rvar, rel')] st'
+ end
+
+fun relation_tac ctxt rel i =
+ TRY (Function_Common.apply_termination_rule ctxt i)
+ THEN PRIMITIVE (inst_thm ctxt rel)
+
+val setup =
+ Method.setup @{binding relation}
+ (Args.term >> (fn rel => fn ctxt => SIMPLE_METHOD' (relation_tac ctxt rel)))
+ "proves termination using a user-specified wellfounded relation"
+
+end
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Oct 25 00:10:25 2009 +0200
@@ -38,8 +38,8 @@
structure ScnpReconstruct : SCNP_RECONSTRUCT =
struct
-val PROFILE = FundefCommon.PROFILE
-fun TRACE x = if ! FundefCommon.profile then tracing x else ()
+val PROFILE = Function_Common.PROFILE
+fun TRACE x = if ! Function_Common.profile then tracing x else ()
open ScnpSolve
@@ -64,7 +64,7 @@
reduction_pair : thm
}
-structure MultisetSetup = TheoryDataFun
+structure Multiset_Setup = TheoryDataFun
(
type T = multiset_setup option
val empty = NONE
@@ -73,10 +73,10 @@
fun merge _ (v1, v2) = if is_some v2 then v2 else v1
)
-val multiset_setup = MultisetSetup.put o SOME
+val multiset_setup = Multiset_Setup.put o SOME
fun undef x = error "undef"
-fun get_multiset_setup thy = MultisetSetup.get thy
+fun get_multiset_setup thy = Multiset_Setup.get thy
|> the_default (Multiset
{ msetT = undef, mk_mset=undef,
mset_regroup_conv=undef, mset_member_tac = undef,
@@ -287,7 +287,7 @@
|> cterm_of thy
in
PROFILE "Proof Reconstruction"
- (CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv sl))) 1
+ (CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv sl))) 1
THEN (rtac @{thm reduction_pair_lemma} 1)
THEN (rtac @{thm rp_inv_image_rp} 1)
THEN (rtac (order_rpair ms_rp label) 1)
@@ -350,7 +350,7 @@
fun single_scnp_tac use_tags orders ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
let
- val ms_configured = is_some (MultisetSetup.get (ProofContext.theory_of ctxt))
+ val ms_configured = is_some (Multiset_Setup.get (ProofContext.theory_of ctxt))
val orders' = if ms_configured then orders
else filter_out (curry op = MS) orders
val gp = gen_probl D cs
@@ -395,7 +395,7 @@
end
fun gen_sizechange_tac orders autom_tac ctxt err_cont =
- TRY (FundefCommon.apply_termination_rule ctxt 1)
+ TRY (Function_Common.apply_termination_rule ctxt 1)
THEN TRY (Termination.wf_union_tac ctxt)
THEN
(rtac @{thm wf_empty} 1
@@ -406,7 +406,7 @@
fun decomp_scnp orders ctxt =
let
- val extra_simps = FundefCommon.Termination_Simps.get ctxt
+ val extra_simps = Function_Common.Termination_Simps.get ctxt
val autom_tac = auto_tac (clasimpset_of ctxt addsimps2 extra_simps)
in
SIMPLE_METHOD
--- a/src/HOL/Tools/Function/scnp_solve.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML Sun Oct 25 00:10:25 2009 +0200
@@ -73,7 +73,7 @@
(* SAT solving *)
val solver = Unsynchronized.ref "auto";
fun sat_solver x =
- FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
+ Function_Common.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
(* "Virtual constructors" for various propositional variables *)
fun var_constrs (gp as GP (arities, gl)) =
--- a/src/HOL/Tools/Function/termination.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML Sun Oct 25 00:10:25 2009 +0200
@@ -48,7 +48,7 @@
structure Termination : TERMINATION =
struct
-open FundefLib
+open Function_Lib
val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord
structure Term2tab = Table(type key = term * term val ord = term2_ord);
@@ -145,7 +145,7 @@
fun mk_sum_skel rel =
let
- val cs = FundefLib.dest_binop_list @{const_name Lattices.sup} rel
+ val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
@@ -233,7 +233,7 @@
fun CALLS tac i st =
if Thm.no_prems st then all_tac st
else case Thm.term_of (Thm.cprem_of st i) of
- (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Lattices.sup} rel, i) st
+ (_ $ (_ $ rel)) => tac (Function_Lib.dest_binop_list @{const_name Lattices.sup} rel, i) st
|_ => no_tac st
type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
@@ -251,7 +251,7 @@
local
fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *)
let
- val (vars, prop) = FundefLib.dest_all_all t
+ val (vars, prop) = Function_Lib.dest_all_all t
val (prems, concl) = Logic.strip_horn prop
val (lhs, rhs) = concl
|> HOLogic.dest_Trueprop
--- a/src/HOL/Tools/inductive.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Sun Oct 25 00:10:25 2009 +0200
@@ -144,7 +144,7 @@
val (tab, monos) = get_inductives ctxt;
val space = Consts.space_of (ProofContext.consts_of ctxt);
in
- [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
+ [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table (space, tab))),
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
|> Pretty.chunks |> Pretty.writeln
end;
--- a/src/HOL/Tools/quickcheck_generators.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Sun Oct 25 00:10:25 2009 +0200
@@ -317,7 +317,7 @@
|> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
|> fold meet_random insts;
in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
- end handle CLASS_ERROR => NONE;
+ end handle Sorts.CLASS_ERROR _ => NONE;
fun ensure_random_datatype config raw_tycos thy =
let
--- a/src/HOL/Tools/record.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/record.ML Sun Oct 25 00:10:25 2009 +0200
@@ -1810,7 +1810,7 @@
fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
let
- val external_names = NameSpace.external_names (Sign.naming_of thy);
+ val external_names = Name_Space.external_names (Sign.naming_of thy);
val alphas = map fst args;
val name = Sign.full_bname thy bname;
--- a/src/HOL/Tools/res_atp.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Sun Oct 25 00:10:25 2009 +0200
@@ -355,7 +355,7 @@
if run_blacklist_filter andalso is_package_def name then I
else
let val xname = Facts.extern facts name in
- if NameSpace.is_hidden xname then I
+ if Name_Space.is_hidden xname then I
else cons (xname, filter_out ResAxioms.bad_for_atp ths)
end) facts [];
--- a/src/Pure/General/markup.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/General/markup.ML Sun Oct 25 00:10:25 2009 +0200
@@ -18,6 +18,9 @@
val kindN: string
val internalK: string
val property_internal: Properties.property
+ val entityN: string val entity: string -> T
+ val defN: string
+ val refN: string
val lineN: string
val columnN: string
val offsetN: string
@@ -161,6 +164,14 @@
val property_internal = (kindN, internalK);
+(* formal entities *)
+
+val (entityN, entity) = markup_string "entity" nameN;
+
+val defN = "def";
+val refN = "ref";
+
+
(* position *)
val lineN = "line";
--- a/src/Pure/General/markup.scala Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/General/markup.scala Sun Oct 25 00:10:25 2009 +0200
@@ -15,6 +15,13 @@
val KIND = "kind"
+ /* formal entities */
+
+ val ENTITY = "entity"
+ val DEF = "def"
+ val REF = "ref"
+
+
/* position */
val LINE = "line"
--- a/src/Pure/General/name_space.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/General/name_space.ML Sun Oct 25 00:10:25 2009 +0200
@@ -20,7 +20,9 @@
val hidden: string -> string
val is_hidden: string -> bool
type T
- val empty: T
+ val empty: string -> T
+ val kind_of: T -> string
+ val the_entry: T -> string -> {is_system: bool, pos: Position.T, id: serial}
val intern: T -> xstring -> string
val extern: T -> string -> xstring
val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
@@ -29,7 +31,7 @@
val merge: T * T -> T
type naming
val default_naming: naming
- val declare: naming -> binding -> T -> string * T
+ val declare: bool -> naming -> binding -> T -> string * T
val full_name: naming -> binding -> string
val external_names: naming -> string -> string list
val add_path: string -> naming -> naming
@@ -37,16 +39,16 @@
val parent_path: naming -> naming
val mandatory_path: string -> naming -> naming
type 'a table = T * 'a Symtab.table
- val define: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
- val empty_table: 'a table
- val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception Symtab.DUP*)
- val join_tables: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*) ->
- 'a table * 'a table -> 'a table (*exception Symtab.DUP*)
+ val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
+ val empty_table: string -> 'a table
+ val merge_tables: 'a table * 'a table -> 'a table
+ val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
+ 'a table * 'a table -> 'a table
val dest_table: 'a table -> (string * 'a) list
val extern_table: 'a table -> (xstring * 'a) list
end;
-structure NameSpace: NAME_SPACE =
+structure Name_Space: NAME_SPACE =
struct
@@ -58,33 +60,71 @@
val is_hidden = String.isPrefix "??.";
+(* datatype entry *)
+
+type entry =
+ {externals: xstring list,
+ is_system: bool,
+ pos: Position.T,
+ id: serial};
+
+fun str_of_entry def (name, {pos, id, ...}: entry) =
+ let
+ val occurrence = (if def then Markup.defN else Markup.refN, string_of_int id);
+ val props = occurrence :: Position.properties_of pos;
+ in Markup.markup (Markup.properties props (Markup.entity name)) name end;
+
+fun err_dup kind entry1 entry2 =
+ error ("Duplicate " ^ kind ^ " declaration " ^
+ quote (str_of_entry true entry1) ^ " vs. " ^ quote (str_of_entry true entry2));
+
+
(* datatype T *)
datatype T =
- NameSpace of
- (string list * string list) Symtab.table * (*internals, hidden internals*)
- xstring list Symtab.table; (*externals*)
+ Name_Space of
+ {kind: string,
+ internals: (string list * string list) Symtab.table, (*visible, hidden*)
+ entries: entry Symtab.table};
+
+fun make_name_space (kind, internals, entries) =
+ Name_Space {kind = kind, internals = internals, entries = entries};
+
+fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
+ make_name_space (f (kind, internals, entries));
+
+fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
+ (kind, Symtab.map_default (xname, ([], [])) f internals, entries));
+
-val empty = NameSpace (Symtab.empty, Symtab.empty);
+fun empty kind = make_name_space (kind, Symtab.empty, Symtab.empty);
+
+fun kind_of (Name_Space {kind, ...}) = kind;
-fun lookup (NameSpace (tab, _)) xname =
- (case Symtab.lookup tab xname of
+fun the_entry (Name_Space {kind, entries, ...}) name =
+ (case Symtab.lookup entries name of
+ NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
+ | SOME {is_system, pos, id, ...} => {is_system = is_system, pos = pos, id = id});
+
+
+(* name accesses *)
+
+fun lookup (Name_Space {internals, ...}) xname =
+ (case Symtab.lookup internals xname of
NONE => (xname, true)
| SOME ([], []) => (xname, true)
| SOME ([name], _) => (name, true)
| SOME (name :: _, _) => (name, false)
| SOME ([], name' :: _) => (hidden name', true));
-fun get_accesses (NameSpace (_, xtab)) name =
- (case Symtab.lookup xtab name of
+fun get_accesses (Name_Space {entries, ...}) name =
+ (case Symtab.lookup entries name of
NONE => [name]
- | SOME xnames => xnames);
+ | SOME {externals, ...} => externals);
-fun put_accesses name xnames (NameSpace (tab, xtab)) =
- NameSpace (tab, Symtab.update (name, xnames) xtab);
-
-fun valid_accesses (NameSpace (tab, _)) name = Symtab.fold (fn (xname, (names, _)) =>
- if not (null names) andalso hd names = name then cons xname else I) tab [];
+fun valid_accesses (Name_Space {internals, ...}) name =
+ Symtab.fold (fn (xname, (names, _)) =>
+ if not (null names) andalso hd names = name then cons xname else I) internals [];
(* intern and extern *)
@@ -116,21 +156,13 @@
unique_names = ! unique_names} space name;
-(* basic operations *)
-
-local
-
-fun map_space f xname (NameSpace (tab, xtab)) =
- NameSpace (Symtab.map_default (xname, ([], [])) f tab, xtab);
+(* modify internals *)
-in
-
-val del_name = map_space o apfst o remove (op =);
-fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
-val add_name = map_space o apfst o update (op =);
-val add_name' = map_space o apsnd o update (op =);
-
-end;
+val del_name = map_internals o apfst o remove (op =);
+fun del_name_extra name =
+ map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
+val add_name = map_internals o apfst o update (op =);
+val add_name' = map_internals o apsnd o update (op =);
(* hide *)
@@ -152,17 +184,24 @@
(* merge *)
-fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
+fun merge
+ (Name_Space {kind = kind1, internals = internals1, entries = entries1},
+ Name_Space {kind = kind2, internals = internals2, entries = entries2}) =
let
- val tab' = (tab1, tab2) |> Symtab.join
+ val kind' =
+ if kind1 = kind2 then kind1
+ else error ("Attempt to merge different kinds of name spaces " ^
+ quote kind1 ^ " vs. " ^ quote kind2);
+ val internals' = (internals1, internals2) |> Symtab.join
(K (fn ((names1, names1'), (names2, names2')) =>
- if pointer_eq (names1, names2) andalso pointer_eq (names1', names2') then raise Symtab.SAME
+ if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
+ then raise Symtab.SAME
else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
- val xtab' = (xtab1, xtab2) |> Symtab.join
- (K (fn xnames =>
- if pointer_eq xnames then raise Symtab.SAME
- else (Library.merge (op =) xnames)));
- in NameSpace (tab', xtab') end;
+ val entries' = (entries1, entries2) |> Symtab.join
+ (fn name => fn (entry1, entry2) =>
+ if #id entry1 = #id entry2 then raise Symtab.SAME
+ else err_dup kind' (name, entry1) (name, entry2));
+ in make_name_space (kind', internals', entries') end;
@@ -225,13 +264,27 @@
(* declaration *)
-fun declare naming binding space =
+fun new_entry strict entry =
+ map_name_space (fn (kind, internals, entries) =>
+ let
+ val entries' =
+ (if strict then Symtab.update_new else Symtab.update) entry entries
+ handle Symtab.DUP dup =>
+ err_dup kind (dup, the (Symtab.lookup entries dup)) entry;
+ in (kind, internals, entries') end);
+
+fun declare strict naming binding space =
let
val names = full naming binding;
val name = Long_Name.implode names;
val _ = name = "" andalso err_bad binding;
val (accs, accs') = accesses naming binding;
- val space' = space |> fold (add_name name) accs |> put_accesses name accs';
+ val entry =
+ {externals = accs',
+ is_system = false,
+ pos = Position.default (Binding.pos_of binding),
+ id = serial ()};
+ val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);
in (name, space') end;
@@ -240,14 +293,14 @@
type 'a table = T * 'a Symtab.table;
-fun define naming (binding, x) (space, tab) =
- let val (name, space') = declare naming binding space
- in (name, (space', Symtab.update_new (name, x) tab)) end;
+fun define strict naming (binding, x) (space, tab) =
+ let val (name, space') = declare strict naming binding space
+ in (name, (space', Symtab.update (name, x) tab)) end;
-val empty_table = (empty, Symtab.empty);
+fun empty_table kind = (empty kind, Symtab.empty);
-fun merge_tables eq ((space1, tab1), (space2, tab2)) =
- (merge (space1, space2), Symtab.merge eq (tab1, tab2));
+fun merge_tables ((space1, tab1), (space2, tab2)) =
+ (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
fun join_tables f ((space1, tab1), (space2, tab2)) =
(merge (space1, space2), Symtab.join f (tab1, tab2));
@@ -261,6 +314,6 @@
end;
-structure Basic_Name_Space: BASIC_NAME_SPACE = NameSpace;
+structure Basic_Name_Space: BASIC_NAME_SPACE = Name_Space;
open Basic_Name_Space;
--- a/src/Pure/General/position.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/General/position.ML Sun Oct 25 00:10:25 2009 +0200
@@ -37,6 +37,7 @@
val range: T -> T -> range
val thread_data: unit -> T
val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
+ val default: T -> T
end;
structure Position: POSITION =
@@ -178,4 +179,8 @@
end;
+fun default pos =
+ if pos = none then thread_data ()
+ else pos;
+
end;
--- a/src/Pure/Isar/attrib.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Oct 25 00:10:25 2009 +0200
@@ -67,35 +67,33 @@
structure Attributes = TheoryDataFun
(
- type T = (((src -> attribute) * string) * stamp) NameSpace.table;
- val empty = NameSpace.empty_table;
+ type T = ((src -> attribute) * string) Name_Space.table;
+ val empty = Name_Space.empty_table "attribute";
val copy = I;
val extend = I;
- fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
- error ("Attempt to merge different versions of attribute " ^ quote dup);
+ fun merge _ tables : T = Name_Space.merge_tables tables;
);
fun print_attributes thy =
let
val attribs = Attributes.get thy;
- fun prt_attr (name, ((_, comment), _)) = Pretty.block
+ fun prt_attr (name, (_, comment)) = Pretty.block
[Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
in
- [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
+ [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table attribs))]
|> Pretty.chunks |> Pretty.writeln
end;
-fun add_attribute name att comment thy = thy |> Attributes.map (fn atts =>
- #2 (NameSpace.define (Sign.naming_of thy) (name, ((att, comment), stamp ())) atts)
- handle Symtab.DUP dup => error ("Duplicate declaration of attribute " ^ quote dup));
+fun add_attribute name att comment thy = thy
+ |> Attributes.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (att, comment)));
(* name space *)
-val intern = NameSpace.intern o #1 o Attributes.get;
+val intern = Name_Space.intern o #1 o Attributes.get;
val intern_src = Args.map_name o intern;
-val extern = NameSpace.extern o #1 o Attributes.get o ProofContext.theory_of;
+val extern = Name_Space.extern o #1 o Attributes.get o ProofContext.theory_of;
(* pretty printing *)
@@ -117,7 +115,7 @@
let val ((name, _), pos) = Args.dest_src src in
(case Symtab.lookup attrs name of
NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
- | SOME ((att, _), _) => (Position.report (Markup.attribute name) pos; att src))
+ | SOME (att, _) => (Position.report (Markup.attribute name) pos; att src))
end;
in attr end;
@@ -340,7 +338,7 @@
Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
Pretty.str (Config.print_value value)]
end;
- val configs = NameSpace.extern_table (#1 (Attributes.get thy), Configs.get thy);
+ val configs = Name_Space.extern_table (#1 (Attributes.get thy), Configs.get thy);
in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
--- a/src/Pure/Isar/isar_cmd.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sun Oct 25 00:10:25 2009 +0200
@@ -400,7 +400,7 @@
val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
val {classes, ...} = Sorts.rep_algebra algebra;
fun entry (c, (i, (_, cs))) =
- (i, {name = NameSpace.extern space c, ID = c, parents = cs,
+ (i, {name = Name_Space.extern space c, ID = c, parents = cs,
dir = "", unfold = true, path = ""});
val gr =
Graph.fold (cons o entry) classes []
--- a/src/Pure/Isar/local_theory.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/Isar/local_theory.ML Sun Oct 25 00:10:25 2009 +0200
@@ -17,7 +17,7 @@
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val raw_theory: (theory -> theory) -> local_theory -> local_theory
val checkpoint: local_theory -> local_theory
- val full_naming: local_theory -> NameSpace.naming
+ val full_naming: local_theory -> Name_Space.naming
val full_name: local_theory -> binding -> string
val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val theory: (theory -> theory) -> local_theory -> local_theory
@@ -139,9 +139,9 @@
fun full_naming lthy =
Sign.naming_of (ProofContext.theory_of lthy)
- |> NameSpace.mandatory_path (#theory_prefix (get_lthy lthy));
+ |> Name_Space.mandatory_path (#theory_prefix (get_lthy lthy));
-fun full_name naming = NameSpace.full_name (full_naming naming);
+fun full_name naming = Name_Space.full_name (full_naming naming);
fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
|> Sign.mandatory_path (#theory_prefix (get_lthy lthy))
--- a/src/Pure/Isar/locale.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/Isar/locale.ML Sun Oct 25 00:10:25 2009 +0200
@@ -124,15 +124,15 @@
structure Locales = TheoryDataFun
(
- type T = locale NameSpace.table;
- val empty = NameSpace.empty_table;
+ type T = locale Name_Space.table;
+ val empty = Name_Space.empty_table "locale";
val copy = I;
val extend = I;
- fun merge _ = NameSpace.join_tables (K merge_locale);
+ fun merge _ = Name_Space.join_tables (K merge_locale);
);
-val intern = NameSpace.intern o #1 o Locales.get;
-val extern = NameSpace.extern o #1 o Locales.get;
+val intern = Name_Space.intern o #1 o Locales.get;
+val extern = Name_Space.extern o #1 o Locales.get;
val get_locale = Symtab.lookup o #2 o Locales.get;
val defined = Symtab.defined o #2 o Locales.get;
@@ -143,7 +143,7 @@
| NONE => error ("Unknown locale " ^ quote name));
fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
- thy |> Locales.map (NameSpace.define (Sign.naming_of thy)
+ thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
(binding,
mk_locale ((parameters, spec, intros, axioms),
((pairself (map (fn decl => (decl, stamp ()))) decls, map (fn n => (n, stamp ())) notes),
@@ -153,7 +153,7 @@
Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
fun print_locales thy =
- Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (Locales.get thy)))
+ Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
|> Pretty.writeln;
--- a/src/Pure/Isar/method.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/Isar/method.ML Sun Oct 25 00:10:25 2009 +0200
@@ -322,32 +322,30 @@
structure Methods = TheoryDataFun
(
- type T = (((src -> Proof.context -> method) * string) * stamp) NameSpace.table;
- val empty = NameSpace.empty_table;
+ type T = ((src -> Proof.context -> method) * string) Name_Space.table;
+ val empty = Name_Space.empty_table "method";
val copy = I;
val extend = I;
- fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
- error ("Attempt to merge different versions of method " ^ quote dup);
+ fun merge _ tables : T = Name_Space.merge_tables tables;
);
fun print_methods thy =
let
val meths = Methods.get thy;
- fun prt_meth (name, ((_, comment), _)) = Pretty.block
+ fun prt_meth (name, (_, comment)) = Pretty.block
[Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
in
- [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
+ [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table meths))]
|> Pretty.chunks |> Pretty.writeln
end;
-fun add_method name meth comment thy = thy |> Methods.map (fn meths =>
- #2 (NameSpace.define (Sign.naming_of thy) (name, ((meth, comment), stamp ())) meths)
- handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup));
+fun add_method name meth comment thy = thy
+ |> Methods.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (meth, comment)));
(* get methods *)
-val intern = NameSpace.intern o #1 o Methods.get;
+val intern = Name_Space.intern o #1 o Methods.get;
val defined = Symtab.defined o #2 o Methods.get;
fun method_i thy =
@@ -357,11 +355,11 @@
let val ((name, _), pos) = Args.dest_src src in
(case Symtab.lookup meths name of
NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
- | SOME ((mth, _), _) => (Position.report (Markup.method name) pos; mth src))
+ | SOME (mth, _) => (Position.report (Markup.method name) pos; mth src))
end;
in meth end;
-fun method thy = method_i thy o Args.map_name (NameSpace.intern (#1 (Methods.get thy)));
+fun method thy = method_i thy o Args.map_name (Name_Space.intern (#1 (Methods.get thy)));
(* method setup *)
--- a/src/Pure/Isar/object_logic.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/Isar/object_logic.ML Sun Oct 25 00:10:25 2009 +0200
@@ -90,7 +90,7 @@
val base_sort = get_base_sort thy;
val b = Binding.map_name (Syntax.type_name mx) a;
val _ = has_duplicates (op =) vs andalso
- error ("Duplicate parameters in type declaration: " ^ quote (Binding.str_of b));
+ error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
val name = Sign.full_name thy b;
val n = length vs;
val T = Type (name, map (fn v => TFree (v, [])) vs);
--- a/src/Pure/Isar/proof_context.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Oct 25 00:10:25 2009 +0200
@@ -21,7 +21,7 @@
val restore_mode: Proof.context -> Proof.context -> Proof.context
val abbrev_mode: Proof.context -> bool
val set_stmt: bool -> Proof.context -> Proof.context
- val naming_of: Proof.context -> NameSpace.naming
+ val naming_of: Proof.context -> Name_Space.naming
val full_name: Proof.context -> binding -> string
val consts_of: Proof.context -> Consts.T
val const_syntax_name: Proof.context -> string -> string
@@ -170,7 +170,7 @@
datatype ctxt =
Ctxt of
{mode: mode, (*inner syntax mode*)
- naming: NameSpace.naming, (*local naming conventions*)
+ naming: Name_Space.naming, (*local naming conventions*)
syntax: LocalSyntax.T, (*local syntax*)
consts: Consts.T * Consts.T, (*local/global consts*)
facts: Facts.T, (*local facts*)
@@ -180,7 +180,7 @@
Ctxt {mode = mode, naming = naming, syntax = syntax,
consts = consts, facts = facts, cases = cases};
-val local_naming = NameSpace.default_naming |> NameSpace.add_path "local";
+val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
structure ContextData = ProofDataFun
(
@@ -231,7 +231,7 @@
map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
val naming_of = #naming o rep_context;
-val full_name = NameSpace.full_name o naming_of;
+val full_name = Name_Space.full_name o naming_of;
val syntax_of = #syntax o rep_context;
val syn_of = LocalSyntax.syn_of o syntax_of;
@@ -924,10 +924,10 @@
(* name space operations *)
-val add_path = map_naming o NameSpace.add_path;
-val mandatory_path = map_naming o NameSpace.mandatory_path;
-val restore_naming = map_naming o K o naming_of;
-val reset_naming = map_naming (K local_naming);
+val add_path = map_naming o Name_Space.add_path;
+val mandatory_path = map_naming o Name_Space.mandatory_path;
+val restore_naming = map_naming o K o naming_of;
+val reset_naming = map_naming (K local_naming);
(* facts *)
@@ -1230,7 +1230,7 @@
| add_abbr (c, (T, SOME t)) =
if not show_globals andalso Symtab.defined globals c then I
else cons (c, Logic.mk_equals (Const (c, T), t));
- val abbrevs = NameSpace.extern_table (space, Symtab.make (Symtab.fold add_abbr consts []));
+ val abbrevs = Name_Space.extern_table (space, Symtab.make (Symtab.fold add_abbr consts []));
in
if null abbrevs andalso not (! verbose) then []
else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
--- a/src/Pure/Thy/thy_output.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/Thy/thy_output.ML Sun Oct 25 00:10:25 2009 +0200
@@ -420,9 +420,9 @@
("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean),
("show_structs", setmp_CRITICAL show_structs o boolean),
("show_question_marks", setmp_CRITICAL show_question_marks o boolean),
- ("long_names", setmp_CRITICAL NameSpace.long_names o boolean),
- ("short_names", setmp_CRITICAL NameSpace.short_names o boolean),
- ("unique_names", setmp_CRITICAL NameSpace.unique_names o boolean),
+ ("long_names", setmp_CRITICAL Name_Space.long_names o boolean),
+ ("short_names", setmp_CRITICAL Name_Space.short_names o boolean),
+ ("unique_names", setmp_CRITICAL Name_Space.unique_names o boolean),
("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
("display", setmp_CRITICAL display o boolean),
("break", setmp_CRITICAL break o boolean),
--- a/src/Pure/Tools/find_theorems.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML Sun Oct 25 00:10:25 2009 +0200
@@ -326,7 +326,7 @@
local
val index_ord = option_ord (K EQUAL);
-val hidden_ord = bool_ord o pairself NameSpace.is_hidden;
+val hidden_ord = bool_ord o pairself Name_Space.is_hidden;
val qual_ord = int_ord o pairself (length o Long_Name.explode);
val txt_ord = int_ord o pairself size;
@@ -355,7 +355,8 @@
val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt));
val shorten =
- NameSpace.extern_flags {long_names = false, short_names = false, unique_names = false} space;
+ Name_Space.extern_flags
+ {long_names = false, short_names = false, unique_names = false} space;
fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
nicer_name (shorten x, i) (shorten y, j)
--- a/src/Pure/codegen.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/codegen.ML Sun Oct 25 00:10:25 2009 +0200
@@ -337,15 +337,16 @@
val tc = Sign.intern_type thy s;
in
case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
- SOME ((Type.LogicalType i, _), _) =>
+ SOME (Type.LogicalType i, _) =>
if num_args_of (fst syn) > i then
error ("More arguments than corresponding type constructor " ^ s)
- else (case AList.lookup (op =) types tc of
- NONE => CodegenData.put {codegens = codegens,
- tycodegens = tycodegens, consts = consts,
- types = (tc, syn) :: types,
- preprocs = preprocs, modules = modules} thy
- | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
+ else
+ (case AList.lookup (op =) types tc of
+ NONE => CodegenData.put {codegens = codegens,
+ tycodegens = tycodegens, consts = consts,
+ types = (tc, syn) :: types,
+ preprocs = preprocs, modules = modules} thy
+ | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
| _ => error ("Not a type constructor: " ^ s)
end;
--- a/src/Pure/consts.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/consts.ML Sun Oct 25 00:10:25 2009 +0200
@@ -11,15 +11,15 @@
val eq_consts: T * T -> bool
val retrieve_abbrevs: T -> string list -> term -> (term * term) list
val dest: T ->
- {constants: (typ * term option) NameSpace.table,
- constraints: typ NameSpace.table}
+ {constants: (typ * term option) Name_Space.table,
+ constraints: typ Name_Space.table}
val the_type: T -> string -> typ (*exception TYPE*)
val the_abbreviation: T -> string -> typ * term (*exception TYPE*)
val type_scheme: T -> string -> typ (*exception TYPE*)
val the_tags: T -> string -> Properties.T (*exception TYPE*)
val is_monomorphic: T -> string -> bool (*exception TYPE*)
val the_constraint: T -> string -> typ (*exception TYPE*)
- val space_of: T -> NameSpace.T
+ val space_of: T -> Name_Space.T
val intern: T -> xstring -> string
val extern: T -> string -> xstring
val extern_early: T -> string -> xstring
@@ -29,9 +29,9 @@
val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
- val declare: bool -> NameSpace.naming -> Properties.T -> (binding * typ) -> T -> T
+ val declare: bool -> Name_Space.naming -> Properties.T -> binding * typ -> T -> T
val constrain: string * typ option -> T -> T
- val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
+ val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string -> Properties.T ->
binding * term -> T -> (term * term) * T
val revert_abbrev: string -> string -> T -> T
val hide: bool -> string -> T -> T
@@ -50,7 +50,7 @@
type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
datatype T = Consts of
- {decls: ((decl * abbrev option) * serial) NameSpace.table,
+ {decls: (decl * abbrev option) Name_Space.table,
constraints: typ Symtab.table,
rev_abbrevs: (term * term) Item_Net.T Symtab.table};
@@ -84,7 +84,7 @@
fun dest (Consts {decls = (space, decls), constraints, ...}) =
{constants = (space,
- Symtab.fold (fn (c, (({T, ...}, abbr), _)) =>
+ Symtab.fold (fn (c, ({T, ...}, abbr)) =>
Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty),
constraints = (space, constraints)};
@@ -93,7 +93,7 @@
fun the_const (Consts {decls = (_, tab), ...}) c =
(case Symtab.lookup tab c of
- SOME (decl, _) => decl
+ SOME decl => decl
| NONE => raise TYPE ("Unknown constant: " ^ quote c, [], []));
fun the_type consts c =
@@ -123,8 +123,8 @@
fun space_of (Consts {decls = (space, _), ...}) = space;
-val intern = NameSpace.intern o space_of;
-val extern = NameSpace.extern o space_of;
+val intern = Name_Space.intern o space_of;
+val extern = Name_Space.extern o space_of;
fun extern_early consts c =
(case try (the_const consts) c of
@@ -221,27 +221,20 @@
(** build consts **)
-fun err_dup_const c =
- error ("Duplicate declaration of constant " ^ quote c);
-
-fun extend_decls naming decl tab = NameSpace.define naming decl tab
- handle Symtab.DUP c => err_dup_const c;
-
-
(* name space *)
fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs) =>
- (apfst (NameSpace.hide fully c) decls, constraints, rev_abbrevs));
+ (apfst (Name_Space.hide fully c) decls, constraints, rev_abbrevs));
(* declarations *)
-fun declare authentic naming tags (b, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
- let
- val tags' = tags |> Position.default_properties (Position.thread_data ());
- val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
- val (_, decls') = decls |> extend_decls naming (b, ((decl, NONE), serial ()));
- in (decls', constraints, rev_abbrevs) end);
+fun declare authentic naming tags (b, declT) =
+ map_consts (fn (decls, constraints, rev_abbrevs) =>
+ let
+ val decl = {T = declT, typargs = typargs_of declT, tags = tags, authentic = authentic};
+ val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
+ in (decls', constraints, rev_abbrevs) end);
(* constraints *)
@@ -278,7 +271,7 @@
val force_expand = mode = PrintMode.internal;
val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
- error ("Illegal schematic variables on rhs of abbreviation: " ^ Binding.str_of b);
+ error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b));
val rhs = raw_rhs
|> Term.map_types (Type.cert_typ tsig)
@@ -286,15 +279,14 @@
|> Term.close_schematic_term;
val normal_rhs = expand_term rhs;
val T = Term.fastype_of rhs;
- val lhs = Const (NameSpace.full_name naming b, T);
+ val lhs = Const (Name_Space.full_name naming b, T);
in
consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
let
- val tags' = tags |> Position.default_properties (Position.thread_data ());
- val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
+ val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true};
val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
val (_, decls') = decls
- |> extend_decls naming (b, ((decl, SOME abbr), serial ()));
+ |> Name_Space.define true naming (b, (decl, SOME abbr));
val rev_abbrevs' = rev_abbrevs
|> insert_abbrevs mode (rev_abbrev lhs rhs);
in (decls', constraints, rev_abbrevs') end)
@@ -313,14 +305,13 @@
(* empty and merge *)
-val empty = make_consts (NameSpace.empty_table, Symtab.empty, Symtab.empty);
+val empty = make_consts (Name_Space.empty_table "constant", Symtab.empty, Symtab.empty);
fun merge
(Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
let
- val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
- handle Symtab.DUP c => err_dup_const c;
+ val decls' = Name_Space.merge_tables (decls1, decls2);
val constraints' = Symtab.join (K fst) (constraints1, constraints2);
val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2);
in make_consts (decls', constraints', rev_abbrevs') end;
--- a/src/Pure/display.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/display.ML Sun Oct 25 00:10:25 2009 +0200
@@ -146,14 +146,14 @@
[Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
val tfrees = map (fn v => TFree (v, []));
- fun pretty_type syn (t, ((Type.LogicalType n, _), _)) =
+ fun pretty_type syn (t, (Type.LogicalType n, _)) =
if syn then NONE
else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
- | pretty_type syn (t, ((Type.Abbreviation (vs, U, syn'), _), _)) =
+ | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
if syn <> syn' then NONE
else SOME (Pretty.block
[prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
- | pretty_type syn (t, ((Type.Nonterminal, _), _)) =
+ | pretty_type syn (t, (Type.Nonterminal, _)) =
if not syn then NONE
else SOME (prt_typ (Type (t, [])));
@@ -179,25 +179,25 @@
val {restricts, reducts} = Defs.dest defs;
val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
val {constants, constraints} = Consts.dest consts;
- val extern_const = NameSpace.extern (#1 constants);
+ val extern_const = Name_Space.extern (#1 constants);
val {classes, default, types, ...} = Type.rep_tsig tsig;
val (class_space, class_algebra) = classes;
val {classes, arities} = Sorts.rep_algebra class_algebra;
- val clsses = NameSpace.dest_table (class_space, Symtab.make (Graph.dest classes));
- val tdecls = NameSpace.dest_table types;
- val arties = NameSpace.dest_table (Sign.type_space thy, arities);
+ val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
+ val tdecls = Name_Space.dest_table types;
+ val arties = Name_Space.dest_table (Sign.type_space thy, arities);
fun prune_const c = not verbose andalso
member (op =) (Consts.the_tags consts c) Markup.property_internal;
- val cnsts = NameSpace.extern_table (#1 constants,
+ val cnsts = Name_Space.extern_table (#1 constants,
Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
- val cnstrs = NameSpace.extern_table constraints;
+ val cnstrs = Name_Space.extern_table constraints;
- val axms = NameSpace.extern_table axioms;
+ val axms = Name_Space.extern_table axioms;
val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
|> map (fn (lhs, rhs) =>
--- a/src/Pure/drule.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/drule.ML Sun Oct 25 00:10:25 2009 +0200
@@ -452,7 +452,7 @@
val read_prop = certify o SimpleSyntax.read_prop;
-fun get_def thy = Thm.axiom thy o NameSpace.intern (Theory.axiom_space thy) o Thm.def_name;
+fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
fun store_thm name th =
Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
--- a/src/Pure/facts.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/facts.ML Sun Oct 25 00:10:25 2009 +0200
@@ -20,7 +20,7 @@
val selections: string * thm list -> (ref * thm) list
type T
val empty: T
- val space_of: T -> NameSpace.T
+ val space_of: T -> Name_Space.T
val intern: T -> xstring -> string
val extern: T -> string -> xstring
val lookup: Context.generic -> T -> string -> (bool * thm list) option
@@ -31,9 +31,9 @@
val props: T -> thm list
val could_unify: T -> term -> thm list
val merge: T * T -> T
- val add_global: NameSpace.naming -> binding * thm list -> T -> string * T
- val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T
- val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T
+ val add_global: Name_Space.naming -> binding * thm list -> T -> string * T
+ val add_local: bool -> Name_Space.naming -> binding * thm list -> T -> string * T
+ val add_dynamic: Name_Space.naming -> binding * (Context.generic -> thm list) -> T -> string * T
val del: string -> T -> T
val hide: bool -> string -> T -> T
end;
@@ -122,11 +122,11 @@
datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
datatype T = Facts of
- {facts: (fact * serial) NameSpace.table,
+ {facts: fact Name_Space.table,
props: thm Net.net};
fun make_facts facts props = Facts {facts = facts, props = props};
-val empty = make_facts NameSpace.empty_table Net.empty;
+val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
(* named facts *)
@@ -136,18 +136,19 @@
val space_of = #1 o facts_of;
val table_of = #2 o facts_of;
-val intern = NameSpace.intern o space_of;
-val extern = NameSpace.extern o space_of;
+val intern = Name_Space.intern o space_of;
+val extern = Name_Space.extern o space_of;
val defined = Symtab.defined o table_of;
fun lookup context facts name =
(case Symtab.lookup (table_of facts) name of
NONE => NONE
- | SOME (Static ths, _) => SOME (true, ths)
- | SOME (Dynamic f, _) => SOME (false, f context));
+ | SOME (Static ths) => SOME (true, ths)
+ | SOME (Dynamic f) => SOME (false, f context));
-fun fold_static f = Symtab.fold (fn (name, (Static ths, _)) => f (name, ths) | _ => I) o table_of;
+fun fold_static f =
+ Symtab.fold (fn (name, Static ths) => f (name, ths) | _ => I) o table_of;
(* content difference *)
@@ -174,61 +175,52 @@
(* merge facts *)
-fun err_dup_fact name = error ("Duplicate fact " ^ quote name);
-
-(* FIXME stamp identity! *)
-fun eq_entry ((Static ths1, _), (Static ths2, _)) = is_equal (list_ord Thm.thm_ord (ths1, ths2))
- | eq_entry ((_, id1: serial), (_, id2)) = id1 = id2;
-
fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
let
- val facts' = NameSpace.merge_tables eq_entry (facts1, facts2)
- handle Symtab.DUP dup => err_dup_fact dup;
+ val facts' = Name_Space.merge_tables (facts1, facts2);
val props' = Net.merge (is_equal o prop_ord) (props1, props2);
in make_facts facts' props' end;
(* add static entries *)
-fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
+local
+
+fun add strict do_props naming (b, ths) (Facts {facts, props}) =
let
- val (name, facts') = if Binding.is_empty b then ("", facts)
- else let
- val (space, tab) = facts;
- val (name, space') = NameSpace.declare naming b space;
- val entry = (name, (Static ths, serial ()));
- val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
- handle Symtab.DUP dup => err_dup_fact dup;
- in (name, (space', tab')) end;
+ val (name, facts') =
+ if Binding.is_empty b then ("", facts)
+ else Name_Space.define strict naming (b, Static ths) facts;
val props' =
- if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
+ if do_props
+ then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
else props;
in (name, make_facts facts' props') end;
-val add_global = add false false;
-val add_local = add true;
+in
+
+val add_global = add true false;
+val add_local = add false;
+
+end;
(* add dynamic entries *)
-fun add_dynamic naming (b, f) (Facts {facts = (space, tab), props}) =
- let
- val (name, space') = NameSpace.declare naming b space;
- val entry = (name, (Dynamic f, serial ()));
- val tab' = Symtab.update_new entry tab
- handle Symtab.DUP dup => err_dup_fact dup;
- in (name, make_facts (space', tab') props) end;
+fun add_dynamic naming (b, f) (Facts {facts, props}) =
+ let val (name, facts') = Name_Space.define true naming (b, Dynamic f) facts;
+ in (name, make_facts facts' props) end;
(* remove entries *)
fun del name (Facts {facts = (space, tab), props}) =
let
- val space' = NameSpace.hide true name space handle ERROR _ => space;
+ val space' = Name_Space.hide true name space handle ERROR _ => space; (* FIXME handle?? *)
val tab' = Symtab.delete_safe name tab;
in make_facts (space', tab') props end;
fun hide fully name (Facts {facts = (space, tab), props}) =
- make_facts (NameSpace.hide fully name space, tab) props;
+ make_facts (Name_Space.hide fully name space, tab) props;
end;
--- a/src/Pure/name.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/name.ML Sun Oct 25 00:10:25 2009 +0200
@@ -45,7 +45,7 @@
(* checked binding *)
-val of_binding = Long_Name.base_name o NameSpace.full_name NameSpace.default_naming;
+val of_binding = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
(* encoded bounds *)
--- a/src/Pure/pure_thy.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/pure_thy.ML Sun Oct 25 00:10:25 2009 +0200
@@ -146,7 +146,7 @@
else
let
val naming = Sign.naming_of thy;
- val name = NameSpace.full_name naming b;
+ val name = Name_Space.full_name naming b;
val (thy', thms') =
register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
val thms'' = map (Thm.transfer thy') thms';
--- a/src/Pure/sign.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/sign.ML Sun Oct 25 00:10:25 2009 +0200
@@ -8,11 +8,11 @@
signature SIGN =
sig
val rep_sg: theory ->
- {naming: NameSpace.naming,
+ {naming: Name_Space.naming,
syn: Syntax.syntax,
tsig: Type.tsig,
consts: Consts.T}
- val naming_of: theory -> NameSpace.naming
+ val naming_of: theory -> Name_Space.naming
val full_name: theory -> binding -> string
val full_name_path: theory -> string -> binding -> string
val full_bname: theory -> bstring -> string
@@ -44,9 +44,9 @@
val const_typargs: theory -> string * typ -> typ list
val const_instance: theory -> string * typ list -> typ
val mk_const: theory -> string * typ list -> term
- val class_space: theory -> NameSpace.T
- val type_space: theory -> NameSpace.T
- val const_space: theory -> NameSpace.T
+ val class_space: theory -> Name_Space.T
+ val type_space: theory -> Name_Space.T
+ val const_space: theory -> Name_Space.T
val intern_class: theory -> xstring -> string
val extern_class: theory -> string -> xstring
val intern_type: theory -> xstring -> string
@@ -137,7 +137,7 @@
(** datatype sign **)
datatype sign = Sign of
- {naming: NameSpace.naming, (*common naming conventions*)
+ {naming: Name_Space.naming, (*common naming conventions*)
syn: Syntax.syntax, (*concrete syntax for terms, types, sorts*)
tsig: Type.tsig, (*order-sorted signature of types*)
consts: Consts.T}; (*polymorphic constants*)
@@ -150,17 +150,17 @@
type T = sign;
val copy = I;
fun extend (Sign {syn, tsig, consts, ...}) =
- make_sign (NameSpace.default_naming, syn, tsig, consts);
+ make_sign (Name_Space.default_naming, syn, tsig, consts);
val empty =
- make_sign (NameSpace.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
+ make_sign (Name_Space.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
fun merge pp (sign1, sign2) =
let
val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
- val naming = NameSpace.default_naming;
+ val naming = Name_Space.default_naming;
val syn = Syntax.merge_syntaxes syn1 syn2;
val tsig = Type.merge_tsigs pp (tsig1, tsig2);
val consts = Consts.merge (consts1, consts2);
@@ -182,10 +182,10 @@
val naming_of = #naming o rep_sg;
-val full_name = NameSpace.full_name o naming_of;
-fun full_name_path thy path = NameSpace.full_name (NameSpace.add_path path (naming_of thy));
+val full_name = Name_Space.full_name o naming_of;
+fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
-fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
+fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
fun full_bname_path thy path = full_name_path thy path o Binding.name;
@@ -240,12 +240,12 @@
val type_space = #1 o #types o Type.rep_tsig o tsig_of;
val const_space = Consts.space_of o consts_of;
-val intern_class = NameSpace.intern o class_space;
-val extern_class = NameSpace.extern o class_space;
-val intern_type = NameSpace.intern o type_space;
-val extern_type = NameSpace.extern o type_space;
-val intern_const = NameSpace.intern o const_space;
-val extern_const = NameSpace.extern o const_space;
+val intern_class = Name_Space.intern o class_space;
+val extern_class = Name_Space.extern o class_space;
+val intern_type = Name_Space.intern o type_space;
+val extern_type = Name_Space.extern o type_space;
+val intern_const = Name_Space.intern o const_space;
+val extern_const = Name_Space.extern o const_space;
val intern_sort = map o intern_class;
val extern_sort = map o extern_class;
@@ -526,8 +526,7 @@
fun declare_const tags ((b, T), mx) thy =
let
val pos = Binding.pos_of b;
- val tags' = Position.default_properties pos tags;
- val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy;
+ val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags [(b, T, mx)] thy;
val _ = Position.report (Markup.const_decl c) pos;
in (const, thy') end;
@@ -612,10 +611,10 @@
(* naming *)
-val add_path = map_naming o NameSpace.add_path;
-val root_path = map_naming NameSpace.root_path;
-val parent_path = map_naming NameSpace.parent_path;
-val mandatory_path = map_naming o NameSpace.mandatory_path;
+val add_path = map_naming o Name_Space.add_path;
+val root_path = map_naming Name_Space.root_path;
+val parent_path = map_naming Name_Space.parent_path;
+val mandatory_path = map_naming o Name_Space.mandatory_path;
fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
--- a/src/Pure/simplifier.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/simplifier.ML Sun Oct 25 00:10:25 2009 +0200
@@ -143,18 +143,14 @@
(** named simprocs **)
-fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name);
-
-
(* data *)
structure Simprocs = GenericDataFun
(
- type T = simproc NameSpace.table;
- val empty = NameSpace.empty_table;
+ type T = simproc Name_Space.table;
+ val empty = Name_Space.empty_table "simproc";
val extend = I;
- fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
- handle Symtab.DUP dup => err_dup_simproc dup;
+ fun merge _ simprocs = Name_Space.merge_tables simprocs;
);
@@ -163,7 +159,7 @@
fun get_simproc context xname =
let
val (space, tab) = Simprocs.get context;
- val name = NameSpace.intern space xname;
+ val name = Name_Space.intern space xname;
in
(case Symtab.lookup tab name of
SOME proc => proc
@@ -201,9 +197,7 @@
val b' = Morphism.binding phi b;
val simproc' = morph_simproc phi simproc;
in
- Simprocs.map (fn simprocs =>
- NameSpace.define naming (b', simproc') simprocs |> snd
- handle Symtab.DUP dup => err_dup_simproc dup)
+ Simprocs.map (#2 o Name_Space.define true naming (b', simproc'))
#> map_ss (fn ss => ss addsimprocs [simproc'])
end)
end;
--- a/src/Pure/theory.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/theory.ML Sun Oct 25 00:10:25 2009 +0200
@@ -19,7 +19,7 @@
val checkpoint: theory -> theory
val copy: theory -> theory
val requires: theory -> string -> string -> unit
- val axiom_space: theory -> NameSpace.T
+ val axiom_space: theory -> Name_Space.T
val axiom_table: theory -> term Symtab.table
val axioms_of: theory -> (string * term) list
val all_axioms_of: theory -> (string * term) list
@@ -80,29 +80,27 @@
perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
datatype thy = Thy of
- {axioms: term NameSpace.table,
+ {axioms: term Name_Space.table,
defs: Defs.T,
wrappers: wrapper list * wrapper list};
fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
-fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
-
structure ThyData = TheoryDataFun
(
type T = thy;
- val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
+ val empty_axioms = Name_Space.empty_table "axiom";
+ val empty = make_thy (empty_axioms, Defs.empty, ([], []));
val copy = I;
- fun extend (Thy {axioms = _, defs, wrappers}) =
- make_thy (NameSpace.empty_table, defs, wrappers);
+ fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);
fun merge pp (thy1, thy2) =
let
val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
- val axioms' = NameSpace.empty_table;
+ val axioms' = empty_axioms;
val defs' = Defs.merge pp (defs1, defs2);
val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
val ens' = Library.merge (eq_snd op =) (ens1, ens2);
@@ -166,7 +164,7 @@
fun read_axm thy (b, str) =
cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in axiom: " ^ quote (Binding.str_of b));
+ cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
(* add_axioms(_i) *)
@@ -176,8 +174,7 @@
fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
let
val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
- val axioms' = fold (snd oo NameSpace.define (Sign.naming_of thy)) axms axioms
- handle Symtab.DUP dup => err_dup_axm dup;
+ val axioms' = fold (#2 oo Name_Space.define true (Sign.naming_of thy)) axms axioms;
in axioms' end);
in
--- a/src/Pure/thm.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/thm.ML Sun Oct 25 00:10:25 2009 +0200
@@ -1724,25 +1724,21 @@
(* authentic derivation names *)
-fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
-
structure Oracles = TheoryDataFun
(
- type T = serial NameSpace.table;
- val empty = NameSpace.empty_table;
+ type T = unit Name_Space.table;
+ val empty = Name_Space.empty_table "oracle";
val copy = I;
val extend = I;
- fun merge _ oracles : T = NameSpace.merge_tables (op =) oracles
- handle Symtab.DUP dup => err_dup_ora dup;
+ fun merge _ oracles : T = Name_Space.merge_tables oracles;
);
-val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get;
+val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get;
fun add_oracle (b, oracle) thy =
let
val naming = Sign.naming_of thy;
- val (name, tab') = NameSpace.define naming (b, serial ()) (Oracles.get thy)
- handle Symtab.DUP _ => err_dup_ora (Binding.str_of b);
+ val (name, tab') = Name_Space.define true naming (b, ()) (Oracles.get thy);
val thy' = Oracles.put tab' thy;
in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
--- a/src/Pure/type.ML Sat Oct 24 20:27:26 2009 +0200
+++ b/src/Pure/type.ML Sun Oct 25 00:10:25 2009 +0200
@@ -14,9 +14,9 @@
Nonterminal
type tsig
val rep_tsig: tsig ->
- {classes: NameSpace.T * Sorts.algebra,
+ {classes: Name_Space.T * Sorts.algebra,
default: sort,
- types: ((decl * Properties.T) * serial) NameSpace.table,
+ types: (decl * Properties.T) Name_Space.table,
log_types: string list}
val empty_tsig: tsig
val defaultS: tsig -> sort
@@ -70,12 +70,12 @@
val eq_type: tyenv -> typ * typ -> bool
(*extend and merge type signatures*)
- val add_class: Pretty.pp -> NameSpace.naming -> binding * class list -> tsig -> tsig
+ val add_class: Pretty.pp -> Name_Space.naming -> binding * class list -> tsig -> tsig
val hide_class: bool -> string -> tsig -> tsig
val set_defsort: sort -> tsig -> tsig
- val add_type: NameSpace.naming -> Properties.T -> binding * int -> tsig -> tsig
- val add_abbrev: NameSpace.naming -> Properties.T -> binding * string list * typ -> tsig -> tsig
- val add_nonterminal: NameSpace.naming -> Properties.T -> binding -> tsig -> tsig
+ val add_type: Name_Space.naming -> Properties.T -> binding * int -> tsig -> tsig
+ val add_abbrev: Name_Space.naming -> Properties.T -> binding * string list * typ -> tsig -> tsig
+ val add_nonterminal: Name_Space.naming -> Properties.T -> binding -> tsig -> tsig
val hide_type: bool -> string -> tsig -> tsig
val add_arity: Pretty.pp -> arity -> tsig -> tsig
val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
@@ -94,18 +94,14 @@
Abbreviation of string list * typ * bool |
Nonterminal;
-fun str_of_decl (LogicalType _) = "logical type constructor"
- | str_of_decl (Abbreviation _) = "type abbreviation"
- | str_of_decl Nonterminal = "syntactic type";
-
(* type tsig *)
datatype tsig =
TSig of {
- classes: NameSpace.T * Sorts.algebra, (*order-sorted algebra of type classes*)
+ classes: Name_Space.T * Sorts.algebra, (*order-sorted algebra of type classes*)
default: sort, (*default sort on input*)
- types: ((decl * Properties.T) * serial) NameSpace.table, (*declared types*)
+ types: (decl * Properties.T) Name_Space.table, (*declared types*)
log_types: string list}; (*logical types sorted by number of arguments*)
fun rep_tsig (TSig comps) = comps;
@@ -113,18 +109,18 @@
fun make_tsig (classes, default, types, log_types) =
TSig {classes = classes, default = default, types = types, log_types = log_types};
-fun build_tsig ((space, classes), default, types) =
+fun build_tsig (classes, default, types) =
let
val log_types =
- Symtab.fold (fn (c, ((LogicalType n, _), _)) => cons (c, n) | _ => I) (snd types) []
- |> Library.sort (Library.int_ord o pairself snd) |> map fst;
- in make_tsig ((space, classes), default, types, log_types) end;
+ Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
+ |> Library.sort (int_ord o pairself snd) |> map fst;
+ in make_tsig (classes, default, types, log_types) end;
fun map_tsig f (TSig {classes, default, types, log_types = _}) =
build_tsig (f (classes, default, types));
val empty_tsig =
- build_tsig ((NameSpace.empty, Sorts.empty_algebra), [], NameSpace.empty_table);
+ build_tsig ((Name_Space.empty "class", Sorts.empty_algebra), [], Name_Space.empty_table "type");
(* classes and sorts *)
@@ -167,7 +163,7 @@
fun undecl_type c = "Undeclared type constructor: " ^ quote c;
-fun lookup_type (TSig {types, ...}) = Option.map fst o Symtab.lookup (snd types);
+fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
fun the_tags tsig c =
(case lookup_type tsig c of
@@ -515,12 +511,12 @@
let
val cs' = map (cert_class tsig) cs
handle TYPE (msg, _, _) => error msg;
- val (c', space') = space |> NameSpace.declare naming c;
+ val (c', space') = space |> Name_Space.declare true naming c;
val classes' = classes |> Sorts.add_class pp (c', cs');
in ((space', classes'), default, types) end);
fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
- ((NameSpace.hide fully c space, classes), default, types));
+ ((Name_Space.hide fully c space, classes), default, types));
(* arities *)
@@ -530,7 +526,7 @@
val _ =
(case lookup_type tsig t of
SOME (LogicalType n, _) => if length Ss <> n then error (bad_nargs t) else ()
- | SOME (decl, _) => error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t)
+ | SOME _ => error ("Logical type constructor expected: " ^ quote t)
| NONE => error (undecl_type t));
val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
handle TYPE (msg, _, _) => error msg;
@@ -559,68 +555,49 @@
local
-fun err_in_decls c decl decl' =
- let val s = str_of_decl decl and s' = str_of_decl decl' in
- if s = s' then error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
- else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
- end;
-
-fun new_decl naming tags (c, decl) (space, types) =
- let
- val tags' = tags |> Position.default_properties (Position.thread_data ());
- val (c', space') = NameSpace.declare naming c space;
- val types' =
- (case Symtab.lookup types c' of
- SOME ((decl', _), _) => err_in_decls c' decl decl'
- | NONE => Symtab.update (c', ((decl, tags'), serial ())) types);
- in (space', types') end;
-
-fun the_decl (_, types) = fst o fst o the o Symtab.lookup types;
+fun new_decl naming tags (c, decl) types =
+ #2 (Name_Space.define true naming (c, (decl, tags)) types);
fun map_types f = map_tsig (fn (classes, default, types) =>
let
val (space', tab') = f types;
- val _ = NameSpace.intern space' "dummy" = "dummy" orelse
+ val _ = Name_Space.intern space' "dummy" = "dummy" orelse
error "Illegal declaration of dummy type";
in (classes, default, (space', tab')) end);
fun syntactic types (Type (c, Ts)) =
- (case Symtab.lookup types c of SOME ((Nonterminal, _), _) => true | _ => false)
+ (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
orelse exists (syntactic types) Ts
| syntactic _ _ = false;
in
fun add_type naming tags (c, n) =
- if n < 0 then error ("Bad type constructor declaration: " ^ quote (Binding.str_of c))
+ if n < 0 then error ("Bad type constructor declaration " ^ quote (Binding.str_of c))
else map_types (new_decl naming tags (c, LogicalType n));
fun add_abbrev naming tags (a, vs, rhs) tsig = tsig |> map_types (fn types =>
let
fun err msg =
- cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote (Binding.str_of a));
+ cat_error msg ("The error(s) above occurred in type abbreviation " ^ quote (Binding.str_of a));
val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
handle TYPE (msg, _, _) => err msg;
- in
- (case duplicates (op =) vs of
- [] => []
- | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
- (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
- [] => []
- | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
- types |> new_decl naming tags (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))
- end);
+ val _ =
+ (case duplicates (op =) vs of
+ [] => []
+ | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
+ val _ =
+ (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
+ [] => []
+ | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
+ in types |> new_decl naming tags (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
fun add_nonterminal naming tags = map_types o new_decl naming tags o rpair Nonterminal;
-fun merge_types (types1, types2) =
- NameSpace.merge_tables (Library.eq_snd (op = : serial * serial -> bool)) (types1, types2)
- handle Symtab.DUP d => err_in_decls d (the_decl types1 d) (the_decl types2 d);
-
end;
fun hide_type fully c = map_tsig (fn (classes, default, (space, types)) =>
- (classes, default, (NameSpace.hide fully c space, types)));
+ (classes, default, (Name_Space.hide fully c space, types)));
(* merge type signatures *)
@@ -632,10 +609,10 @@
val (TSig {classes = (space2, classes2), default = default2, types = types2,
log_types = _}) = tsig2;
- val space' = NameSpace.merge (space1, space2);
+ val space' = Name_Space.merge (space1, space2);
val classes' = Sorts.merge_algebra pp (classes1, classes2);
val default' = Sorts.inter_sort classes' (default1, default2);
- val types' = merge_types (types1, types2);
+ val types' = Name_Space.merge_tables (types1, types2);
in build_tsig ((space', classes'), default', types') end;
end;