# HG changeset patch # User wenzelm # Date 1256421957 -7200 # Node ID 9d7d0bef2a777ddffbfe7c1e55387cee88fd81a2 # Parent 9d501e11084a72f9f9174b8cd0d54e5926f46ffa# Parent e3463e6db704b5d18c072d48595cfe2dda72e67a merged diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/FunDef.thy Sun Oct 25 00:05:57 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 \ 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])) *} diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/IsaMakefile Sun Oct 25 00:05:57 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 \ diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Library/Multiset.thy Sun Oct 25 00:05:57 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 = diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/SizeChange/sct.ML --- a/src/HOL/SizeChange/sct.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/SizeChange/sct.ML Sun Oct 25 00:05:57 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) = diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/auto_term.ML --- a/src/HOL/Tools/Function/auto_term.ML Sat Oct 24 21:30:33 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/context_tree.ML --- a/src/HOL/Tools/Function/context_tree.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Tools/Function/context_tree.ML Sun Oct 25 00:05:57 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/decompose.ML --- a/src/HOL/Tools/Function/decompose.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Tools/Function/decompose.ML Sun Oct 25 00:05:57 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) diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/descent.ML --- a/src/HOL/Tools/Function/descent.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Tools/Function/descent.ML Sun Oct 25 00:05:57 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/fun.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Function/fun.ML Sun Oct 25 00:05:57 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/function.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Function/function.ML Sun Oct 25 00:05:57 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/function_common.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Function/function_common.ML Sun Oct 25 00:05:57 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 + diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/function_core.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Function/function_core.ML Sun Oct 25 00:05:57 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/function_lib.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Function/function_lib.ML Sun Oct 25 00:05:57 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/fundef.ML --- a/src/HOL/Tools/Function/fundef.ML Sat Oct 24 21:30:33 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/fundef_common.ML --- a/src/HOL/Tools/Function/fundef_common.ML Sat Oct 24 21:30:33 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 - diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/fundef_core.ML --- a/src/HOL/Tools/Function/fundef_core.ML Sat Oct 24 21:30:33 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/fundef_datatype.ML --- a/src/HOL/Tools/Function/fundef_datatype.ML Sat Oct 24 21:30:33 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/fundef_lib.ML --- a/src/HOL/Tools/Function/fundef_lib.ML Sat Oct 24 21:30:33 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/induction_scheme.ML --- a/src/HOL/Tools/Function/induction_scheme.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Tools/Function/induction_scheme.ML Sun Oct 25 00:05:57 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/inductive_wrap.ML --- a/src/HOL/Tools/Function/inductive_wrap.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Tools/Function/inductive_wrap.ML Sun Oct 25 00:05:57 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Sun Oct 25 00:05:57 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; diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Tools/Function/mutual.ML Sun Oct 25 00:05:57 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' diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/pat_completeness.ML --- a/src/HOL/Tools/Function/pat_completeness.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Tools/Function/pat_completeness.ML Sun Oct 25 00:05:57 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) diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/pattern_split.ML --- a/src/HOL/Tools/Function/pattern_split.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Tools/Function/pattern_split.ML Sun Oct 25 00:05:57 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 __ *) diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/relation.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Function/relation.ML Sun Oct 25 00:05:57 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/scnp_reconstruct.ML --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Oct 25 00:05:57 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 diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/scnp_solve.ML --- a/src/HOL/Tools/Function/scnp_solve.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Tools/Function/scnp_solve.ML Sun Oct 25 00:05:57 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)) = diff -r 9d501e11084a -r 9d7d0bef2a77 src/HOL/Tools/Function/termination.ML --- a/src/HOL/Tools/Function/termination.ML Sat Oct 24 21:30:33 2009 +0200 +++ b/src/HOL/Tools/Function/termination.ML Sun Oct 25 00:05:57 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