--- a/src/HOL/Tools/function_package/fundef_package.ML Wed Sep 13 00:38:38 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Sep 13 12:05:50 2006 +0200
@@ -1,4 +1,3 @@
-
(* Title: HOL/Tools/function_package/fundef_package.ML
ID: $Id$
Author: Alexander Krauss, TU Muenchen
@@ -10,7 +9,17 @@
signature FUNDEF_PACKAGE =
sig
- val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list -> bool -> theory -> Proof.state (* Need an _i variant *)
+ val add_fundef : (string * string option * mixfix) list
+ -> ((bstring * Attrib.src list) * string list) list list
+ -> bool
+ -> local_theory
+ -> Proof.state
+
+ val add_fundef_i: (string * typ option * mixfix) list
+ -> ((bstring * Attrib.src list) * term list) list list
+ -> bool
+ -> local_theory
+ -> Proof.state
val cong_add: attribute
val cong_del: attribute
@@ -20,167 +29,136 @@
end
-structure FundefPackage : FUNDEF_PACKAGE =
+structure FundefPackage =
struct
open FundefCommon
-fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy =
- let
- val psimpss = Library.unflat (map snd spec_part) psimps
- val (names, attss) = split_list (map fst spec_part)
+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
- val thy = thy |> Theory.add_path f_name
+fun restore_spec_structure reps spec =
+ (burrow o burrow_snd o burrow o K) reps spec
- val thy = thy |> Theory.add_path label
- val spsimpss = map (map standard) psimpss (* FIXME *)
- val add_list = (names ~~ spsimpss) ~~ attss
- val (_, thy) = PureThy.add_thmss add_list thy
- val thy = thy |> Theory.parent_path
-
- val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy
- val thy = thy |> Theory.parent_path
+fun with_local_path path f lthy =
+ let
+ val restore = Theory.restore_naming (ProofContext.theory_of lthy)
in
- thy
+ lthy
+ |> LocalTheory.theory (Theory.add_path path)
+ |> f
+ |> LocalTheory.theory restore
end
-
-
-
-
-
-fun fundef_afterqed congs mutual_info name data spec [[result]] thy =
+fun add_simps label moreatts mutual_info fixes psimps spec lthy =
let
- val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
- val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
- val Mutual {parts, ...} = mutual_info
+ val fnames = map (fst o fst) fixes
+ val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames psimps
- val Prep {names = Names {acc_R=accR, ...}, ...} = data
- val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
- val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
-
- val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) spec thy
-
- val casenames = flat (map (map (fst o fst)) spec)
-
- val thy = thy |> Theory.add_path name
- val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy
- val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
- val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
- val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy
- val thy = thy |> Theory.parent_path
+ fun add_for_f fname psimps =
+ with_local_path fname
+ (LocalTheory.note ((label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd)
in
- add_fundef_data name (fundef_data, mutual_info, spec) thy
- end
-
-fun gen_add_fundef prep_att eqns_attss (preprocess : bool) thy =
- let
- fun prep_eqns neqs =
- neqs
- |> map (apsnd (Sign.read_prop thy))
- |> map (apfst (apsnd (apfst (map (prep_att thy)))))
- |> FundefSplit.split_some_equations (ProofContext.init thy)
-
- val spec = map prep_eqns eqns_attss
- val t_eqnss = map (flat o map snd) spec
-
- val congs = get_fundef_congs (Context.Theory thy)
-
- val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy
- val Prep {goal, goalI, ...} = data
- in
- thy |> ProofContext.init
- |> Proof.theorem_i PureThy.internalK NONE
- (ProofContext.theory o fundef_afterqed congs mutual_info name data spec) NONE ("", [])
- [(("", []), [(goal, [])])]
- |> Proof.refine (Method.primitive_text (fn _ => goalI))
- |> Seq.hd
+ lthy
+ |> fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) |> snd
+ |> fold2 add_for_f fnames psimps_by_f
end
-fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy =
+fun fundef_afterqed fixes spec mutual_info defname data [[result]] lthy =
+ let
+ 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
+ in
+ lthy
+ |> add_simps "psimps" [] mutual_info fixes psimps spec
+ |> with_local_path defname
+ (LocalTheory.note (("domintros", []), domintros) #> snd
+ #> LocalTheory.note (("termination", []), [termination]) #> snd
+ #> LocalTheory.note (("cases", []), [cases]) #> snd
+ #> LocalTheory.note (("pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) #> snd)
+ |> LocalTheory.theory (Context.theory_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))))
+ end (* FIXME: Add cases for induct and cases thm *)
+
+
+
+fun prep_with_flags prep fixspec eqnss_flags global_flag lthy =
let
- val totality = hd (hd thmss)
+ val eqnss = map (map (apsnd (map fst))) eqnss_flags
+ val flags = map (map (map (fn (_, f) => global_flag orelse f) o snd)) eqnss_flags
+
+ val ((fixes, _), ctxt') = prep fixspec [] lthy
+ val spec = map (fn eqns => snd (fst (prep [] eqns ctxt'))) eqnss
+ |> map (map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)))) (* Add quantifiers *)
+ |> map2 (map2 (fn fs => fn (r, thms) => (r, fs ~~ thms))) flags
+ |> (burrow o burrow_snd o burrow)
+ (FundefSplit.split_some_equations lthy)
+ |> map (map (apsnd flat))
+ in
+ ((fixes, spec), ctxt')
+ end
+
- val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
- = the (get_fundef_data name thy)
+fun gen_add_fundef prep_spec fixspec eqnss_flags preprocess lthy =
+ let
+ val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags preprocess lthy
+ 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 lthy
+
+ val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
+ in
+ lthy
+ |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
+ |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd
+ end
+
+
+fun total_termination_afterqed defname data [[totality]] lthy =
+ let
+ val (FundefMResult {psimps, simple_pinducts, ... }, mutual_info, (fixes, stmts)) = data
val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
- val tsimps = map (map remove_domain_condition) psimps
+ val tsimps = map remove_domain_condition psimps
val tinduct = map remove_domain_condition simple_pinducts
- val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps)
- val allatts = if has_guards then [] else [RecfunCodegen.add NONE]
-
- val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy
-
- val thy = Theory.add_path name thy
-
- val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy
- val thy = Theory.parent_path thy
+ (* FIXME: How to generate code from (possibly) local contexts
+ val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
+ val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
+ *)
in
- thy
- end
-
-(*
-fun mk_partial_rules name D_name D domT idomT thmss thy =
- let
- val [subs, dcl] = (hd thmss)
-
- val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
- = the (Symtab.lookup (FundefData.get thy) name)
-
- val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)]
- [SOME (cterm_of thy D)]
- subsetD)
-
- val D_simps = map (curry op RS D_implies_dom) f_simps
-
- val D_induct = subset_induct
- |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
- |> curry op COMP subs
- |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
- |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
-
- val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
- val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
- in
- thy3
- end
-*)
-
-
-fun fundef_setup_termination_proof name NONE thy =
- let
- val name = if name = "" then get_last_fundef thy else name
- val data = the (get_fundef_data name thy)
- handle Option.Option => raise ERROR ("No such function definition: " ^ name)
-
- val (res as FundefMResult {termination, ...}, mutual, _) = data
- val goal = FundefTermination.mk_total_termination_goal data
- in
- thy |> ProofContext.init
- |> ProofContext.note_thmss_i [(("termination",
- [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd
- |> Proof.theorem_i PureThy.internalK NONE
- (ProofContext.theory o total_termination_afterqed name mutual) NONE ("", [])
- [(("", []), [(goal, [])])]
- end
- | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
- let
- val name = if name = "" then get_last_fundef thy else name
- val data = the (get_fundef_data name thy)
- val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
- in
- thy |> ProofContext.init
- |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
- [(("", []), [(subs, []), (dcl, [])])]
+ lthy
+ |> add_simps "simps" [] mutual_info fixes tsimps stmts
+ |> with_local_path defname
+ (LocalTheory.note (("induct", [Attrib.internal (InductAttrib.induct_set "")]), tinduct) #> snd)
end
-val add_fundef = gen_add_fundef Attrib.attribute
+fun fundef_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 (res as FundefMResult {termination, ...}, _, _) = data
+ val goal = FundefTermination.mk_total_termination_goal data
+ in
+ lthy
+ |> ProofContext.note_thmss_i [(("termination",
+ [ContextRules.intro_query NONE]), [(ProofContext.export_standard lthy lthy [termination], [])])] |> snd
+ |> Proof.theorem_i PureThy.internalK NONE
+ (total_termination_afterqed name data) NONE ("", [])
+ [(("", []), [(goal, [])])]
+ end
+
+
+val add_fundef = gen_add_fundef Specification.read_specification
+val add_fundef_i = gen_add_fundef Specification.cert_specification
@@ -206,39 +184,34 @@
-val star = Scan.one (fn t => (OuterLex.val_of t = "*"));
+fun or_list1 s = P.enum1 "|" s
+
+val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
+
+val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
+val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
+val statements_ow = or_list1 statement_ow
-val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME))
- >> (fn x => (map_filter I x, exists is_none x)))
- --| P.$$$ "]";
-
-val opt_attribs_with_star = Scan.optional attribs_with_star ([], false);
-
-val opt_thm_name_star =
- Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ ":") ("", ([], false));
-
-
-val function_decl =
- Scan.repeat1 (opt_thm_name_star -- P.prop);
+fun local_theory_to_proof f =
+ Toplevel.theory_to_proof (f o LocalTheory.init NONE)
val functionP =
OuterSyntax.command "function" "define general recursive functions" K.thy_goal
- (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) --
- P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
- Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
+ ((opt_sequential -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
+ >> (fn (((sequential, target), fixes), statements) =>
+ Toplevel.print o local_theory_to_proof (add_fundef fixes statements sequential)));
+
val terminationP =
OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
- ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
- >> (fn (name,dom) =>
- Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
+ (Scan.option P.name
+ >> (fn name => Toplevel.print o local_theory_to_proof (fundef_setup_termination_proof name)));
-val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
val _ = OuterSyntax.add_parsers [functionP];
val _ = OuterSyntax.add_parsers [terminationP];
-
+val _ = OuterSyntax.add_keywords ["sequential", "otherwise"]; (* currently unused *)
end;