# HG changeset patch # User krauss # Date 1169483383 -3600 # Node ID 0a50d4db234a13039a95c2098e603712f4c716e8 # Parent eaec72532dd768d29159b55ce67d72c94f49de1e * Preliminary implementation of tail recursion * Clarified internal interfaces diff -r eaec72532dd7 -r 0a50d4db234a src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Mon Jan 22 16:53:33 2007 +0100 +++ b/src/HOL/FunDef.thy Mon Jan 22 17:29:43 2007 +0100 @@ -13,13 +13,11 @@ ("Tools/function_package/fundef_lib.ML") ("Tools/function_package/inductive_wrap.ML") ("Tools/function_package/context_tree.ML") -("Tools/function_package/fundef_prep.ML") -("Tools/function_package/fundef_proof.ML") +("Tools/function_package/fundef_core.ML") ("Tools/function_package/termination.ML") ("Tools/function_package/mutual.ML") ("Tools/function_package/pattern_split.ML") ("Tools/function_package/fundef_package.ML") -(*("Tools/function_package/fundef_datatype.ML")*) ("Tools/function_package/auto_term.ML") begin @@ -71,6 +69,27 @@ done +lemma not_accP_down: + assumes na: "\ accP R x" + obtains z where "R z x" and "\accP R z" +proof - + assume a: "\z. \R z x; \ accP R z\ \ thesis" + + show thesis + proof (cases "\z. R z x \ accP R z") + case True + hence "\z. R z x \ accP R z" by auto + hence "accP R x" + by (rule accPI) + with na show thesis .. + next + case False then obtain z where "R z x" and "\accP R z" + by auto + with a show thesis . + qed +qed + + lemma accP_subset: assumes sub: "\x y. R1 x y \ R2 x y" shows "\x. accP R2 x \ accP R1 x" @@ -195,8 +214,7 @@ use "Tools/function_package/fundef_lib.ML" use "Tools/function_package/inductive_wrap.ML" use "Tools/function_package/context_tree.ML" -use "Tools/function_package/fundef_prep.ML" -use "Tools/function_package/fundef_proof.ML" +use "Tools/function_package/fundef_core.ML" use "Tools/function_package/termination.ML" use "Tools/function_package/mutual.ML" use "Tools/function_package/pattern_split.ML" diff -r eaec72532dd7 -r 0a50d4db234a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Jan 22 16:53:33 2007 +0100 +++ b/src/HOL/IsaMakefile Mon Jan 22 17:29:43 2007 +0100 @@ -107,8 +107,7 @@ Tools/function_package/fundef_datatype.ML \ Tools/function_package/fundef_lib.ML \ Tools/function_package/fundef_package.ML \ - Tools/function_package/fundef_prep.ML \ - Tools/function_package/fundef_proof.ML \ + Tools/function_package/fundef_core.ML \ Tools/function_package/inductive_wrap.ML \ Tools/function_package/lexicographic_order.ML \ Tools/function_package/mutual.ML \ diff -r eaec72532dd7 -r 0a50d4db234a src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Mon Jan 22 16:53:33 2007 +0100 +++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Jan 22 17:29:43 2007 +0100 @@ -12,7 +12,6 @@ (* Theory Dependencies *) val acc_const_name = "FunDef.accP" -val domintros = ref true; val profile = ref false; fun PROFILE msg = if !profile then timeap_msg msg else I @@ -20,6 +19,7 @@ fun mk_acc domT R = Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R +(* FIXME, unused *) val function_name = suffix "C" val graph_name = suffix "_graph" val rel_name = suffix "_rel" @@ -35,163 +35,29 @@ | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list) | RCall of (term * ctx_tree) -type glrs = (term list * term list * term * term) list -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: ctx_tree, - lGI: thm, - RCs: rec_call_info list - } - - - - -type qgar = string * (string * typ) list * term list * term list * term - -fun name_of_fqgar (f, _, _, _, _) = f - -datatype mutual_part = - MutualPart of - { - fvar : string * typ, - cargTs: typ list, - pthA: SumTools.sum_path, - pthR: SumTools.sum_path, - f_def: term, - - f: term option, - f_defthm : thm option - } - - -datatype mutual_info = - Mutual of - { - defname: string, - fsum_var : string * typ, - - ST: typ, - RST: typ, - streeA: SumTools.sum_tree, - streeR: SumTools.sum_tree, - - parts: mutual_part list, - fqgars: qgar list, - qglrs: ((string * typ) list * term list * term * term) list, - - fsum : term option - } - - -datatype prep_result = - Prep of - { - globals: globals, - f: term, - G: term, - R: term, - - goal: term, - goalI: thm, - values: thm list, - clauses: clause_info list, - - R_cases: thm, - ex1_iff: thm - } - datatype fundef_result = FundefResult of { f: term, - G : term, - R : term, - completeness : thm, - - psimps : thm list, - subset_pinduct : thm, - simple_pinduct : thm, - total_intro : thm, - dom_intros : thm list - } - -datatype fundef_mresult = - FundefMResult of - { - f: term, G: term, R: term, psimps : thm list, + trsimps : thm list option, + subset_pinducts : thm list, simple_pinducts : thm list, cases : thm, termination : thm, - domintros : thm list + domintros : thm list option } datatype fundef_context_data = FundefCtxData of { - fixes : ((string * typ) * mixfix) list, - spec : ((string * Attrib.src list) * term list) list list, - mutual: mutual_info, + add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory, f : term, R : term, @@ -261,6 +127,7 @@ | Preprocessor of string | Target of xstring | DomIntros + | Tailrec datatype fundef_config = FundefConfig of @@ -269,23 +136,29 @@ default: string, preprocessor: string option, target: xstring option, - domintros: bool + domintros: bool, + tailrec: bool } -val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false } -val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false } +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, + target=NONE, domintros=false, tailrec=false } + +val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, + target=NONE, domintros=false, tailrec=false } -fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros}) = - FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros } - | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros}) = - FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros } - | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros}) = - FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros } - | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros }) = - FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros } - | apply_opt Domintros (FundefConfig {sequential, default, preprocessor, target, domintros }) = - FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true } +fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = + FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec } + | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = + FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec } + | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = + FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros, tailrec=tailrec } + | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = + FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros, tailrec=tailrec } + | apply_opt DomIntros (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = + FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true,tailrec=tailrec } + | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = + FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true } local structure P = OuterParse and K = OuterKeyword in @@ -295,29 +168,18 @@ val option_parser = (P.$$$ "sequential" >> K Sequential) || ((P.reserved "default" |-- P.term) >> Default) || (P.reserved "domintros" >> K DomIntros) + || (P.reserved "tailrec" >> K Tailrec) || ((P.$$$ "in" |-- P.xname) >> Target) fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") []) >> (fn opts => fold apply_opt opts def) + end - - - - - - - - - - - - - end diff -r eaec72532dd7 -r 0a50d4db234a src/HOL/Tools/function_package/fundef_core.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/function_package/fundef_core.ML Mon Jan 22 17:29:43 2007 +0100 @@ -0,0 +1,952 @@ +(* Title: HOL/Tools/function_package/fundef_core.ML + ID: $Id$ + Author: Alexander Krauss, TU Muenchen + +A package for general recursive function definitions. +Main functionality +*) + +signature FUNDEF_CORE = +sig + val prepare_fundef : FundefCommon.fundef_config + -> string (* defname *) + -> (string * typ * mixfix) (* defined symbol *) + -> ((string * typ) list * term list * term * term) list (* specification *) + -> string (* default_value, not parsed yet *) + -> local_theory + + -> (term (* f *) + * thm (* goalstate *) + * (thm -> FundefCommon.fundef_result) (* continuation *) + ) * local_theory + +end + +structure FundefCore : FUNDEF_CORE = +struct + + +open FundefLib +open FundefCommon +open FundefAbbrev + +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: ctx_tree, + lGI: thm, + RCs: rec_call_info list + } + + +(* Theory dependencies. *) +val Pair_inject = thm "Product_Type.Pair_inject"; + +val acc_induct_rule = thm "FunDef.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 "FunDef.accP_downward" +val accI = thm "FunDef.accPI" +val case_split = thm "HOL.case_split_thm" +val fundef_default_value = thm "FunDef.fundef_default_value" +val not_accP_down = thm "FunDef.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 + (implies $ Trueprop (eq_const domT $ shift lhs $ lhs') + $ Trueprop (eq_const ranT $ shift rhs $ rhs')) + |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') + |> fold_rev (fn (n,T) => fn b => 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, _, _, _)) = + Trueprop Pbool + |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs))) + |> fold_rev (curry Logic.mk_implies) gs + |> fold_rev mk_forall_rename (map fst oqs ~~ qs) + in + 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 (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 *) +fun abstract_over_list vs body = + let + exception SAME; + 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 handle SAME => u) handle SAME => t $ abs lev v u) + | _ => raise SAME); + in + fold_index (fn (i,v) => fn t => abs i v t handle SAME => 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 implies_elim_swp 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 implies_elim_swp ags + |> fold implies_elim_swp rcassm + + val h_assum = + Trueprop (G $ rcarg $ (h $ rcarg)) + |> fold_rev (curry Logic.mk_implies o prop_of) rcassm + |> fold_rev (mk_forall 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 (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 implies_elim_swp agsj + |> fold implies_elim_swp agsi + |> implies_elim_swp ((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 implies_elim_swp agsi + |> fold implies_elim_swp agsj + |> implies_elim_swp (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 + + val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) 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 ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *) + + val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (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 + |> Goal.close_result + 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 implies_elim_swp agsj' + |> fold implies_elim_swp Ghsj' + + val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h)))) + val lhsi_eq_lhsj' = assume (cterm_of thy (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 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 (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 + |> implies_elim_swp G_lhs_y + |> fold implies_elim_swp 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 thy congs globals G f R clauses complete compat compat_store G_elim f_def = + let + val Globals {h, domT, ranT, x, ...} = globals + + (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) + val ihyp = all domT $ Abs ("z", domT, + implies $ Trueprop (R $ Bound 0 $ x) + $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $ + Abs ("y", ranT, G $ Bound 1 $ Bound 0))) + |> cterm_of thy + + val ihyp_thm = assume ihyp |> 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) + + val _ = Output.debug (K "Proving Replacement lemmas...") + val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses + + val _ = Output.debug (K "Proving cases for unique existence...") + val (ex1s, values) = + split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) + + val _ = Output.debug (K "Proving: Graph is a function") (* FIXME: Rewrite this proof. *) + val graph_is_function = complete + |> forall_elim_vars 0 + |> fold (curry op COMP) ex1s + |> implies_intr (ihyp) + |> implies_intr (cterm_of thy (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) (term_vars (prop_of it)) it) + + val goalstate = Conjunction.intr graph_is_function complete + |> Goal.close_result + |> 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) = + Trueprop (Gvar $ rcarg $ (fvar $ rcarg)) + |> fold_rev (curry Logic.mk_implies o prop_of) rcassm + |> fold_rev (mk_forall o Free) rcfix + in + Trueprop (Gvar $ lhs $ rhs) + |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs + |> fold_rev (curry Logic.mk_implies) gs + |> fold_rev mk_forall (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 ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $ + Abs ("y", ranT, G $ Bound 1 $ Bound 0)) + |> Envir.beta_norm (* FIXME: LocalTheory.def does not work if not beta-normal *) + + val ((f, (_, f_defthm)), lthy) = + LocalTheory.def Thm.internalK ((fname ^ "C", mixfix), ((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) = + Trueprop (Rvar $ rcarg $ lhs) + |> fold_rev (curry Logic.mk_implies o prop_of) rcassm + |> fold_rev (curry Logic.mk_implies) gs + |> fold_rev (mk_forall 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 (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) + val z_smaller = cterm_of thy (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 "FunDef.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 (Trueprop (D $ x))) + val a_D = cterm_of thy (Trueprop (D $ a)) + + val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x))) + + val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) + mk_forall x + (mk_forall z (Logic.mk_implies (Trueprop (D $ x), + Logic.mk_implies (Trueprop (R $ z $ x), + Trueprop (D $ z))))) + |> cterm_of thy + + + (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) + val ihyp = all domT $ Abs ("z", domT, + implies $ Trueprop (R $ Bound 0 $ x) + $ Trueprop (P $ Bound 0)) + |> cterm_of thy + + val aihyp = assume ihyp + + fun prove_case clause = + let + val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, + qglr = (oqs, _, _, _), ...} = clause + + val replace_x_ss = HOL_basic_ss addsimps [case_hyp] + val lhs_D = simplify replace_x_ss x_D (* lhs : D *) + val sih = full_simplify replace_x_ss aihyp + + fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = + sih |> forall_elim (cterm_of thy rcarg) + |> implies_elim_swp 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 = 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 (Trueprop (D $ lhs)) + |> fold_rev mk_forall_rename (map fst oqs ~~ qs) + |> cterm_of thy + + val P_lhs = assume step + |> fold forall_elim cqs + |> implies_elim_swp lhs_D + |> fold_rev implies_elim_swp ags + |> fold implies_elim_swp P_recs + + val res = cterm_of thy (Trueprop (P $ x)) + |> Simplifier.rewrite replace_x_ss + |> 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 + |> 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 + (subset_induct_all, simple_induct_rule) + end + + + +(* FIXME: This should probably use fixed goals, to be more reliable and faster *) +fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause = + let + val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, + qglr = (oqs, _, _, _), ...} = clause + val goal = 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 [forall_elim_vars 0 R_cases] 1)) |> the + |> (SINGLE (CLASIMPSET auto_tac)) |> the + |> Goal.conclude + |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) + end + + + +(** Termination rule **) + +val wf_induct_rule = thm "FunDef.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 ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub) + + val hyp = Trueprop (R' $ arg $ lhs) + |> fold_rev (curry Logic.mk_implies o prop_of) used + |> FundefCtxTree.export_term (fixes, map prop_of 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 implies_elim_swp ags + |> FundefCtxTree.import_thm thy (fixes, assumes) (* "(arg, lhs) : R'" *) + |> fold implies_elim_swp used + + val acc = thm COMP ih_case + + val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg))) + + val arg_eq_z = (assume z_eq_arg) RS sym + + val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *) + |> implies_intr (cprop_of case_hyp) + |> implies_intr z_eq_arg + + val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg)))) + val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs)))) + + val ethm = (z_acc OF [z_eq_arg, x_eq_lhs]) + |> FundefCtxTree.export_thm thy (fixes, + prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (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", mk_relT (domT, domT)) + val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel + + val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *) + + (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) + val ihyp = all domT $ Abs ("z", domT, + implies $ Trueprop (R' $ Bound 0 $ x) + $ Trueprop (acc_R $ Bound 0)) + |> cterm_of thy + + val ihyp_a = assume ihyp |> forall_elim_vars 0 + + val R_z_x = cterm_of thy (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') + |> 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 = 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 (SIMPSET' asm_full_simp_tac)) 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" *) + in + Goal.prove ctxt [] [] trsimp + (fn _ => + rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1 + THEN (rtac (forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1 + THEN (SIMPSET (fn ss => asm_full_simp_tac (ss addsimps [default_thm]) 1)) + THEN (etac not_accP_down 1) + THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps [default_thm])))) 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 default_str lthy = + let + val FundefConfig {domintros, tailrec, ...} = config + + val fvar = Free (fname, fT) + val domT = domain_type fT + val ranT = range_type fT + + val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *) + + val congs = get_fundef_congs (Context.Proof 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 + + val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *) + + fun build_tree (ClauseContext { ctxt, rhs, ...}) = + FundefCtxTree.mk_tree congs_deps (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 ^ "_sum_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.default_mode ((defname ^ "_dom", 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 newthy congs 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 (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 (subset_pinduct, 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 newthy globals R R_elim)) xclauses) + else NONE + val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE + + in + FundefResult {f=f, G=G, R=R, cases=complete_thm, + psimps=psimps, subset_pinducts=[subset_pinduct], simple_pinducts=[simple_pinduct], + termination=total_intro, trsimps=trsimps, + domintros=dom_intros} + end + in + ((f, goalstate, mk_partial_rules), lthy) + end + + + + +end diff -r eaec72532dd7 -r 0a50d4db234a src/HOL/Tools/function_package/fundef_lib.ML --- a/src/HOL/Tools/function_package/fundef_lib.ML Mon Jan 22 16:53:33 2007 +0100 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Jan 22 17:29:43 2007 +0100 @@ -10,14 +10,34 @@ structure FundefLib = struct +(* ==> library/string *) fun plural sg pl [x] = sg | plural sg pl _ = pl + + +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); + + + + + + +(* ??? *) fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *) +(* ==> logic.ML? *) fun mk_forall v t = all (fastype_of v) $ lambda v t -(* Constructs a tupled abstraction from an arbitrarily nested tuple of variables and a term. *) +(* lambda-abstracts over an arbitrarily nested tuple + ==> hologic.ML? *) fun tupled_lambda vars t = case vars of (Free v) => lambda (Free v) t @@ -86,16 +106,12 @@ (* 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. Probably quicker than Pattern.rewrite_terms, and 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) - - +(* term.ML *) fun forall_aterms P (t $ u) = forall_aterms P t andalso forall_aterms P u | forall_aterms P (Abs (_, _, t)) = forall_aterms P t | forall_aterms P a = P a @@ -104,6 +120,11 @@ +(* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and 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 @@ -116,7 +137,7 @@ fun forall_intr_rename (n, cv) thm = let val allthm = forall_intr cv thm - val (_, abs) = Logic.dest_all (prop_of allthm) + val (_ $ abs) = prop_of allthm in Thm.rename_boundvars abs (Abs (n, dummyT, dummy_term)) allthm end @@ -127,11 +148,6 @@ Term.add_frees t [] |> filter_out (Variable.is_fixed ctxt o fst) |> rev -(* - rev (fold_aterms (fn Free (v as (x, _)) => - if Variable.is_fixed ctxt x then I else insert (fn ((x, _),(y, _)) => x = y) v | _ => I) t []) -*) - end diff -r eaec72532dd7 -r 0a50d4db234a src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Mon Jan 22 16:53:33 2007 +0100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Jan 22 17:29:43 2007 +0100 @@ -40,6 +40,8 @@ val note_theorem = LocalTheory.note Thm.theoremK +fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" + fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *) let val (xs, ys) = split_list ps in xs ~~ f ys end @@ -47,49 +49,46 @@ fun restore_spec_structure reps spec = (burrow o burrow_snd o burrow o K) reps spec -fun add_simps label moreatts mutual_info fixes psimps spec lthy = +fun add_simps fixes spec sort label moreatts simps lthy = let val fnames = map (fst o fst) fixes - val (saved_spec_psimps, lthy) = - fold_map (fold_map note_theorem) (restore_spec_structure psimps spec) lthy - val saved_psimps = flat (map snd (flat saved_spec_psimps)) + val (saved_spec_simps, lthy) = + fold_map (fold_map note_theorem) (restore_spec_structure simps spec) lthy + val saved_simps = flat (map snd (flat saved_spec_simps)) - val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps + val simps_by_f = sort saved_simps - fun add_for_f fname psimps = + fun add_for_f fname simps = note_theorem ((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts), - psimps) #> snd + simps) #> snd in - (saved_psimps, - fold2 add_for_f fnames psimps_by_f lthy) + (saved_simps, + fold2 add_for_f fnames simps_by_f lthy) end -fun fundef_afterqed config fixes spec mutual_info defname data [[result]] lthy = +fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy = let - val FundefConfig { domintros, ...} = config - val Prep {f, R, ...} = data - val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result - val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data + val FundefResult {f, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = + cont (Goal.close_result proof) + val qualify = NameSpace.qualified defname + val addsimps = add_simps fixes spec sort_cont val (((psimps', pinducts'), (_, [termination'])), lthy) = lthy - |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec) - ||>> PROFILE "adding pinduct" - (note_theorem ((qualify "pinduct", - [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts)) - ||>> PROFILE "adding termination" - (note_theorem ((qualify "termination", []), [termination])) - ||> (snd o PROFILE "adding cases" (note_theorem ((qualify "cases", []), [cases]))) - ||> (snd o PROFILE "adding domintros" (note_theorem ((qualify "domintros", []), domintros))) + |> addsimps "psimps" [] psimps + ||> fold_option (snd oo addsimps "simps" []) trsimps + ||>> note_theorem ((qualify "pinduct", + [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts) + ||>> note_theorem ((qualify "termination", []), [termination]) + ||> (snd o note_theorem ((qualify "cases", []), [cases])) + ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros - val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps', + val cdata = FundefCtxData { add_simps=addsimps, psimps=psimps', pinducts=snd pinducts', termination=termination', f=f, R=R } - - in lthy (* FIXME proper handling of morphism *) |> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *) @@ -117,33 +116,36 @@ fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy = let - val FundefConfig {sequential, default, ...} = config + val FundefConfig {sequential, default, tailrec, ...} = config val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy + + val defname = mk_defname fixes + val t_eqns = spec |> flat |> map snd |> flat (* flatten external structure *) - val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) = - FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy + val ((goalstate, cont, sort_cont), lthy) = + FundefMutual.prepare_fundef_mutual config defname fixes t_eqns default lthy - val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result + val afterqed = fundef_afterqed config fixes spec defname cont sort_cont in - (name, lthy - |> Proof.theorem_i NONE afterqed [[(goal, [])]] - |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd) + (defname, lthy + |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]] + |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd) end fun total_termination_afterqed defname data [[totality]] lthy = let - val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data + val FundefCtxData { add_simps, psimps, pinducts, ... } = data - val totality = PROFILE "closing" Goal.close_result totality + val totality = Goal.close_result totality val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) - val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps - val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts + val tsimps = map remove_domain_condition psimps + val tinduct = map remove_domain_condition pinducts (* FIXME: How to generate code from (possibly) local contexts*) val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps @@ -152,26 +154,26 @@ val qualify = NameSpace.qualified defname; in lthy - |> PROFILE "adding tsimps" (add_simps "simps" allatts mutual fixes tsimps spec) |> snd - |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd + |> add_simps "simps" allatts tsimps |> snd + |> note_theorem ((qualify "induct", []), tinduct) |> snd end fun setup_termination_proof name_opt lthy = let - val name = the_default (get_last_fundef (Context.Proof lthy)) name_opt - val data = the (get_fundef_data name (Context.Proof lthy)) - handle Option.Option => raise ERROR ("No such function definition: " ^ name) + val defname = the_default (get_last_fundef (Context.Proof lthy)) name_opt + val data = the (get_fundef_data defname (Context.Proof lthy)) + handle Option.Option => raise ERROR ("No such function definition: " ^ defname) - val FundefCtxData {termination, f, R, ...} = data - val goal = FundefTermination.mk_total_termination_goal f R + val FundefCtxData {termination, R, ...} = data + val goal = FundefTermination.mk_total_termination_goal R in lthy |> ProofContext.note_thmss_i "" [(("termination", [ContextRules.intro_query NONE]), [([Goal.norm_result termination], [])])] |> snd |> set_termination_rule termination - |> Proof.theorem_i NONE (total_termination_afterqed name data) [[(goal, [])]] + |> Proof.theorem_i NONE (total_termination_afterqed defname data) [[(goal, [])]] end diff -r eaec72532dd7 -r 0a50d4db234a src/HOL/Tools/function_package/fundef_prep.ML --- a/src/HOL/Tools/function_package/fundef_prep.ML Mon Jan 22 16:53:33 2007 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,534 +0,0 @@ -(* Title: HOL/Tools/function_package/fundef_prep.ML - ID: $Id$ - Author: Alexander Krauss, TU Muenchen - -A package for general recursive function definitions. -Preparation step: makes auxiliary definitions and generates -proof obligations. -*) - -signature FUNDEF_PREP = -sig - val prepare_fundef : string (* defname *) - -> (string * typ * mixfix) (* defined symbol *) - -> ((string * typ) list * term list * term * term) list (* specification *) - -> string (* default_value, not parsed yet *) - -> local_theory - -> FundefCommon.prep_result * term * local_theory - -end - -structure FundefPrep : FUNDEF_PREP = -struct - - -open FundefLib -open FundefCommon -open FundefAbbrev - -(* Theory dependencies. *) -val Pair_inject = thm "Product_Type.Pair_inject"; - -val acc_induct_rule = thm "FunDef.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 conjunctionI = thm "conjunctionI"; - - - -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 - - -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 - (implies $ Trueprop (eq_const domT $ shift lhs $ lhs') - $ Trueprop (eq_const ranT $ shift rhs $ rhs')) - |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') - |> fold_rev (fn (n,T) => fn b => 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, _, _, _)) = - Trueprop Pbool - |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs))) - |> fold_rev (curry Logic.mk_implies) gs - |> fold_rev mk_forall_rename (map fst oqs ~~ qs) - in - Trueprop Pbool - |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) - |> mk_forall_rename ("x", x) - |> mk_forall_rename ("P", Pbool) - end - - -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 (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 *) -fun abstract_over_list vs body = - let - exception SAME; - 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 handle SAME => u) handle SAME => t $ abs lev v u) - | _ => raise SAME); - in - fold_index (fn (i,v) => fn t => abs i v t handle SAME => 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 implies_elim_swp 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 implies_elim_swp ags - |> fold implies_elim_swp rcassm - - val h_assum = - Trueprop (G $ rcarg $ (h $ rcarg)) - |> fold_rev (curry Logic.mk_implies o prop_of) rcassm - |> fold_rev (mk_forall 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 (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 implies_elim_swp agsj - |> fold implies_elim_swp agsi - |> implies_elim_swp ((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 implies_elim_swp agsi - |> fold implies_elim_swp agsj - |> implies_elim_swp (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 - - val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) 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 ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *) - - val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (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 - |> Goal.close_result - 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 implies_elim_swp agsj' - |> fold implies_elim_swp Ghsj' - - val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h)))) - val lhsi_eq_lhsj' = assume (cterm_of thy (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 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 (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 - |> implies_elim_swp G_lhs_y - |> fold implies_elim_swp 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 thy congs globals G f R clauses complete compat compat_store G_elim f_def = - let - val Globals {h, domT, ranT, x, ...} = globals - - val inst_ex1_ex = f_def RS ex1_implies_ex - val inst_ex1_un = f_def RS ex1_implies_un - val inst_ex1_iff = f_def RS ex1_implies_iff - - (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) - val ihyp = all domT $ Abs ("z", domT, - implies $ Trueprop (R $ Bound 0 $ x) - $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $ - Abs ("y", ranT, G $ Bound 1 $ Bound 0))) - |> cterm_of thy - - val ihyp_thm = assume ihyp |> forall_elim_vars 0 - val ih_intro = ihyp_thm RS inst_ex1_ex - val ih_elim = ihyp_thm RS inst_ex1_un - - val _ = Output.debug (fn () => "Proving Replacement lemmas...") - val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses - - val _ = Output.debug (fn () => "Proving cases for unique existence...") - val (ex1s, values) = - split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) - - val _ = Output.debug (fn () => "Proving: Graph is a function") (* FIXME: Rewrite this proof. *) - val graph_is_function = complete - |> forall_elim_vars 0 - |> fold (curry op COMP) ex1s - |> implies_intr (ihyp) - |> implies_intr (cterm_of thy (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) (term_vars (prop_of it)) it) - - val goal = complete COMP (graph_is_function COMP conjunctionI) - |> Goal.close_result - - val goalI = Goal.protect goal - |> fold_rev (implies_intr o cprop_of) compat - |> implies_intr (cprop_of complete) - in - (prop_of goal, goalI, inst_ex1_iff, 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) = - Trueprop (Gvar $ rcarg $ (fvar $ rcarg)) - |> fold_rev (curry Logic.mk_implies o prop_of) rcassm - |> fold_rev (mk_forall o Free) rcfix - in - Trueprop (Gvar $ lhs $ rhs) - |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs - |> fold_rev (curry Logic.mk_implies) gs - |> fold_rev mk_forall (fvar :: qs) - end - - val G_intros = map2 mk_GIntro clauses RCss - - val (GIntro_thms, (G, G_elim, lthy)) = - FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy) - in - ((G, GIntro_thms, G_elim), lthy) - end - - - -fun define_function fdefname (fname, mixfix) domT ranT G default lthy = - let - val f_def = - Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $ - Abs ("y", ranT, G $ Bound 1 $ Bound 0)) - |> Envir.beta_norm (* FIXME: LocalTheory.def does not work if not beta-normal *) - - val ((f, (_, f_defthm)), lthy) = - LocalTheory.def Thm.internalK ((fname ^ "C", mixfix), ((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) = - Trueprop (Rvar $ rcarg $ lhs) - |> fold_rev (curry Logic.mk_implies o prop_of) rcassm - |> fold_rev (curry Logic.mk_implies) gs - |> fold_rev (mk_forall 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 - - - -fun prepare_fundef defname (fname, fT, mixfix) abstract_qglrs default_str lthy = - let - val fvar = Free (fname, fT) - val domT = domain_type fT - val ranT = range_type fT - - val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *) - - val congs = get_fundef_congs (Context.Proof lthy) - val (globals, ctxt') = fix_globals domT ranT fvar lthy - - val Globals { x, h, ... } = globals - - val clauses = PROFILE "mk_clause_context" (map (mk_clause_context x ctxt')) abstract_qglrs - - val n = length abstract_qglrs - - val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *) - - fun build_tree (ClauseContext { ctxt, rhs, ...}) = - FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs - - val trees = PROFILE "making trees" (map build_tree) clauses - val RCss = PROFILE "finding calls" (map find_calls) trees - - val ((G, GIntro_thms, G_elim), 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 ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy - - val RCss = PROFILE "inst_RCs" (map (map (inst_RC (ProofContext.theory_of lthy) fvar f))) RCss - val trees = PROFILE "inst_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) = PROFILE "abbrev" - (LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", 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 = PROFILE "mk_compl" (mk_completeness globals clauses) abstract_qglrs |> cert |> assume - val compat = PROFILE "mk_compat" (mk_compat_proof_obligations domT ranT fvar f) abstract_qglrs |> map (cert #> assume) - - val compat_store = store_compat_thms n compat - - val (goal, goalI, ex1_iff, values) = PROFILE "prove_stuff" (prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm - in - (Prep {globals = globals, f = f, G = G, R = R, goal = goal, goalI = goalI, values = values, clauses = xclauses, ex1_iff = ex1_iff, R_cases = R_elim}, f, - lthy) - end - - - - -end diff -r eaec72532dd7 -r 0a50d4db234a src/HOL/Tools/function_package/fundef_proof.ML --- a/src/HOL/Tools/function_package/fundef_proof.ML Mon Jan 22 16:53:33 2007 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,327 +0,0 @@ -(* Title: HOL/Tools/function_package/fundef_proof.ML - ID: $Id$ - Author: Alexander Krauss, TU Muenchen - -A package for general recursive function definitions. -Internal proofs. -*) - - -signature FUNDEF_PROOF = -sig - - val mk_partial_rules : theory -> FundefCommon.prep_result - -> thm -> FundefCommon.fundef_result -end - - -structure FundefProof : FUNDEF_PROOF = -struct - -open FundefLib -open FundefCommon -open FundefAbbrev - -(* Theory dependencies *) -val subsetD = thm "subsetD" -val split_apply = thm "Product_Type.split" -val wf_induct_rule = thm "FunDef.wfP_induct_rule"; -val Pair_inject = thm "Product_Type.Pair_inject"; - -val wf_in_rel = thm "FunDef.wf_in_rel"; -val in_rel_def = thm "FunDef.in_rel_def"; - -val acc_induct_rule = thm "FunDef.accP_induct_rule" -val acc_downward = thm "FunDef.accP_downward" -val accI = thm "FunDef.accPI" - -val acc_subset_induct = thm "FunDef.accP_subset_induct" - -val conjunctionD1 = thm "conjunctionD1" -val conjunctionD2 = thm "conjunctionD2" - - -fun mk_psimp thy globals R f_iff graph_is_function clause valthm = - let - val Globals {domT, z, ...} = globals - - val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause - val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) - val z_smaller = cterm_of thy (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 - - - -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 (Trueprop (D $ x))) - val a_D = cterm_of thy (Trueprop (D $ a)) - - val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x))) - - val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) - mk_forall x - (mk_forall z (Logic.mk_implies (Trueprop (D $ x), - Logic.mk_implies (Trueprop (R $ z $ x), - Trueprop (D $ z))))) - |> cterm_of thy - - - (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) - val ihyp = all domT $ Abs ("z", domT, - implies $ Trueprop (R $ Bound 0 $ x) - $ Trueprop (P $ Bound 0)) - |> cterm_of thy - - val aihyp = assume ihyp - - fun prove_case clause = - let - val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, rhs, case_hyp, ...}, RCs, - qglr = (oqs, _, _, _), ...} = clause - - val replace_x_ss = HOL_basic_ss addsimps [case_hyp] - val lhs_D = simplify replace_x_ss x_D (* lhs : D *) - val sih = full_simplify replace_x_ss aihyp - - fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = - sih |> forall_elim (cterm_of thy rcarg) - |> implies_elim_swp 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 = 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 (Trueprop (D $ lhs)) - |> fold_rev mk_forall_rename (map fst oqs ~~ qs) - |> cterm_of thy - - val P_lhs = assume step - |> fold forall_elim cqs - |> implies_elim_swp lhs_D - |> fold_rev implies_elim_swp ags - |> fold implies_elim_swp P_recs - - val res = cterm_of thy (Trueprop (P $ x)) - |> Simplifier.rewrite replace_x_ss - |> 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 - |> 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 - (subset_induct_all, simple_induct_rule) - end - - - -(* Does this work with Guards??? *) -fun mk_domain_intro thy globals R R_cases clause = - let - val Globals {z, domT, ...} = globals - val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, - qglr = (oqs, _, _, _), ...} = clause - val goal = 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 [forall_elim_vars 0 R_cases] 1)) |> the - |> (SINGLE (CLASIMPSET auto_tac)) |> the - |> Goal.conclude - |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) - end - - -fun maybe_mk_domain_intro thy = - if !FundefCommon.domintros then mk_domain_intro thy - else K (K (K (K refl))) - - -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 ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub) - - val hyp = Trueprop (R' $ arg $ lhs) - |> fold_rev (curry Logic.mk_implies o prop_of) used - |> FundefCtxTree.export_term (fixes, map prop_of 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 implies_elim_swp ags - |> FundefCtxTree.import_thm thy (fixes, assumes) (* "(arg, lhs) : R'" *) - |> fold implies_elim_swp used - - val acc = thm COMP ih_case - - val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg))) - - val arg_eq_z = (assume z_eq_arg) RS sym - - val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *) - |> implies_intr (cprop_of case_hyp) - |> implies_intr z_eq_arg - - val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg)))) - val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs)))) - - val ethm = (z_acc OF [z_eq_arg, x_eq_lhs]) - |> FundefCtxTree.export_thm thy (fixes, - prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (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", mk_relT (domT, domT)) - val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel - - val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *) - - (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) - val ihyp = all domT $ Abs ("z", domT, - implies $ Trueprop (R' $ Bound 0 $ x) - $ Trueprop (acc_R $ Bound 0)) - |> cterm_of thy - - val ihyp_a = assume ihyp |> forall_elim_vars 0 - - val R_z_x = cterm_of thy (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') - |> 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 - - - - -fun mk_partial_rules thy data provedgoal = - let - val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data - - val provedgoal = PROFILE "Closing result" Goal.close_result provedgoal - - val graph_is_function = PROFILE "Getting function theorem" (fn x => (x COMP conjunctionD1) |> forall_elim_vars 0) provedgoal - - val complete_thm = PROFILE "Getting cases" (curry op COMP provedgoal) conjunctionD2 - - val f_iff = PROFILE "Making f_iff" (curry op RS graph_is_function) ex1_iff - - val psimps = PROFILE "Proving simplification rules" (map2 (mk_psimp thy globals R f_iff graph_is_function)) clauses values - - val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule" - (mk_partial_induct_rule thy globals R complete_thm) clauses - - val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule thy globals R R_cases) clauses - - val dom_intros = PROFILE "Proving domain introduction rules" (map (maybe_mk_domain_intro thy globals R R_cases)) clauses - in - FundefResult {f=f, G=G, R=R, completeness=complete_thm, - psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro, - dom_intros=dom_intros} - end - - -end - - diff -r eaec72532dd7 -r 0a50d4db234a src/HOL/Tools/function_package/inductive_wrap.ML --- a/src/HOL/Tools/function_package/inductive_wrap.ML Mon Jan 22 16:53:33 2007 +0100 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML Mon Jan 22 17:29:43 2007 +0100 @@ -11,7 +11,7 @@ sig val inductive_def : term list -> ((bstring * typ) * mixfix) * local_theory - -> thm list * (term * thm * local_theory) + -> thm list * (term * thm * thm * local_theory) end structure FundefInductiveWrap = @@ -40,7 +40,7 @@ let val qdefs = map dest_all_all defs - val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], ...}, lthy) = + val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) = InductivePackage.add_inductive_i true (*verbose*) "" (* no altname *) false (* no coind *) @@ -70,7 +70,7 @@ |> Term.strip_comb |> snd |> hd (* Trueprop *) |> Term.strip_comb |> fst in - (intrs, (Rdef_real, elim, lthy)) + (intrs, (Rdef_real, elim, induct, lthy)) end end diff -r eaec72532dd7 -r 0a50d4db234a src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Mon Jan 22 16:53:33 2007 +0100 +++ b/src/HOL/Tools/function_package/mutual.ML Mon Jan 22 17:29:43 2007 +0100 @@ -9,17 +9,16 @@ signature FUNDEF_MUTUAL = sig - val prepare_fundef_mutual : ((string * typ) * mixfix) list + val prepare_fundef_mutual : FundefCommon.fundef_config + -> string (* defname *) + -> ((string * typ) * mixfix) list -> term list -> string (* default, unparsed term *) -> local_theory - -> ((FundefCommon.mutual_info * string * FundefCommon.prep_result) * local_theory) - - - val mk_partial_rules_mutual : Proof.context -> FundefCommon.mutual_info -> FundefCommon.prep_result -> thm -> - FundefCommon.fundef_mresult - - val sort_by_function : FundefCommon.mutual_info -> string list -> 'a list -> 'a list list + -> ((thm (* goalstate *) + * (thm -> FundefCommon.fundef_result) (* proof continuation *) + * (thm list -> thm list list) (* sorting continuation *) + ) * local_theory) end @@ -34,6 +33,45 @@ val sum_case_rules = thms "Datatype.sum.cases" val split_apply = thm "Product_Type.split" +type qgar = string * (string * typ) list * term list * term list * term + +fun name_of_fqgar (f, _, _, _, _) = f + +datatype mutual_part = + MutualPart of + { + fvar : string * typ, + cargTs: typ list, + pthA: SumTools.sum_path, + pthR: SumTools.sum_path, + f_def: term, + + f: term option, + f_defthm : thm option + } + + +datatype mutual_info = + Mutual of + { + fsum_var : string * typ, + + ST: typ, + RST: typ, + streeA: SumTools.sum_tree, + streeR: SumTools.sum_tree, + + parts: mutual_part list, + fqgars: qgar list, + qglrs: ((string * typ) list * term list * term * term) list, + + fsum : term option + } + + + + + fun mutual_induct_Pnames n = @@ -100,7 +138,7 @@ end; -fun analyze_eqs ctxt fs eqs = +fun analyze_eqs ctxt defname fs eqs = let val fnames = map fst fs val (fqgars, arities) = fold_map (split_def ctxt fnames) eqs Symtab.empty @@ -119,10 +157,9 @@ val (RST,streeR, pthsR) = SumTools.mk_tree_distinct resultTs val (ST, streeA, pthsA) = SumTools.mk_tree argTs - val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name fnames) val fsum_type = ST --> RST - val ([fsum_var_name], _) = Variable.add_fixes [ def_name ^ "_sum" ] ctxt + val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt val fsum_var = (fsum_var_name, fsum_type) fun define (fvar as (n, T)) caTs pthA pthR = @@ -150,7 +187,7 @@ val qglrs = map convert_eqs fqgars in - Mutual {defname=def_name,fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, + Mutual {fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE} end @@ -171,29 +208,15 @@ lthy') end - val Mutual { defname, fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual + val Mutual { fsum_var, ST, RST, streeA, streeR, parts, fqgars, qglrs, ... } = mutual val (parts', lthy') = fold_map def (parts ~~ fixes) lthy in - (Mutual { defname=defname, fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts', + (Mutual { fsum_var=fsum_var, ST=ST, RST=RST, streeA=streeA, streeR=streeR, parts=parts', fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum }, lthy') end -fun prepare_fundef_mutual fixes eqss default lthy = - let - val mutual = analyze_eqs lthy (map fst fixes) eqss - val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual - - val (prep_result, fsum, lthy') = - FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy - - val (mutual', lthy'') = define_projections fixes mutual fsum lthy' - in - ((mutual', defname, prep_result), lthy'') - end - - (* Beta-reduce both sides of a meta-equality *) fun beta_norm_eq thm = let @@ -315,7 +338,7 @@ -fun mk_partial_rules_mutual lthy (m as Mutual {RST, parts, streeR, fqgars, ...}) data prep_result = +fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {RST, parts, streeR, fqgars, ...}) proof = let val thy = ProofContext.theory_of lthy @@ -323,8 +346,9 @@ val expand = Assumption.export false lthy (LocalTheory.target_of lthy) val expand_term = Drule.term_rule thy expand - val result = FundefProof.mk_partial_rules thy data prep_result - val FundefResult {f, G, R, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = result + val result = inner_cont proof + val FundefResult {f, G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct], + termination,domintros} = result val all_f_defs = map (fn MutualPart {f_defthm = SOME f_def, cargTs, ...} => mk_applied_form lthy cargTs (symmetric (Thm.freezeT f_def))) @@ -333,18 +357,19 @@ fun mk_mpsimp fqgar sum_psimp = in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp - val mpsimps = PROFILE "making mpsimps" (map2 mk_mpsimp fqgars) psimps - val minducts = PROFILE "making mpinduct" (mutual_induct_rules thy simple_pinduct all_f_defs) m - val termination = PROFILE "making mtermination" (full_simplify (HOL_basic_ss addsimps all_f_defs)) total_intro + val mpsimps = map2 mk_mpsimp fqgars psimps + val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps + val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m + val mtermination = full_simplify (HOL_basic_ss addsimps all_f_defs) termination in - FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R, - psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts, - cases=expand completeness, termination=expand termination, - domintros=map expand dom_intros } + FundefResult { f=expand_term f, G=expand_term G, R=expand_term R, + psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts, + cases=expand cases, termination=expand mtermination, + domintros=map_option (map expand) domintros, + trsimps=map_option (map expand) trsimps} end - - + (* puts an object in the "right bucket" *) fun store_grouped P x [] = [] | store_grouped P x ((l, xs)::bs) = @@ -356,5 +381,23 @@ (map (rpair []) names) (* in the empty buckets labeled with names *) |> map (snd #> map snd) (* and remove the labels afterwards *) + + +fun prepare_fundef_mutual config defname fixes eqss default lthy = + let + val mutual = analyze_eqs lthy defname (map fst fixes) eqss + val Mutual {fsum_var=(n, T), qglrs, ...} = mutual + + val ((fsum, goalstate, cont), lthy') = + FundefCore.prepare_fundef config defname (n, T, NoSyn) qglrs default lthy + + val (mutual', lthy'') = define_projections fixes mutual fsum lthy' + + val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual' + val sort_cont = sort_by_function mutual' (map (fst o fst) fixes) + in + ((goalstate, mutual_cont, sort_cont), lthy'') + end + end diff -r eaec72532dd7 -r 0a50d4db234a src/HOL/Tools/function_package/termination.ML --- a/src/HOL/Tools/function_package/termination.ML Mon Jan 22 16:53:33 2007 +0100 +++ b/src/HOL/Tools/function_package/termination.ML Mon Jan 22 17:29:43 2007 +0100 @@ -9,7 +9,7 @@ signature FUNDEF_TERMINATION = sig - val mk_total_termination_goal : term -> term -> term + val mk_total_termination_goal : term -> term (* val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term*) end @@ -21,9 +21,9 @@ open FundefCommon open FundefAbbrev -fun mk_total_termination_goal f R = +fun mk_total_termination_goal R = let - val domT = domain_type (fastype_of f) + val domT = domain_type (fastype_of R) val x = Free ("x", domT) in mk_forall x (Trueprop (mk_acc domT R $ x)) diff -r eaec72532dd7 -r 0a50d4db234a src/HOL/ex/Fundefs.thy --- a/src/HOL/ex/Fundefs.thy Mon Jan 22 16:53:33 2007 +0100 +++ b/src/HOL/ex/Fundefs.thy Mon Jan 22 17:29:43 2007 +0100 @@ -24,7 +24,6 @@ text {* There is also a cases rule to distinguish cases along the definition *} thm fib.cases -thm fib.domintros text {* total simp and induction rules: *} thm fib.simps @@ -172,8 +171,6 @@ thm evn_od.pinduct thm evn_od.termination -thm evn_od.domintros -