# HG changeset patch # User krauss # Date 1158834125 -7200 # Node ID d80502f0d7018ca9f46c9056c16061583670bdfa # Parent 24cda2c5fd40d30a034b49be42b3628c959915ba 1. Function package accepts a parameter (default "some_term"), which specifies the functions behaviour outside its domain. 2. Bugfix: An exception occured when a function in a mutual definition was declared but no equation was given. diff -r 24cda2c5fd40 -r d80502f0d701 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Thu Sep 21 03:17:51 2006 +0200 +++ b/src/HOL/FunDef.thy Thu Sep 21 12:22:05 2006 +0200 @@ -41,25 +41,45 @@ lemma fundef_ex1_existence: -assumes f_def: "f \ \x. THE_default d (\y. (x,y)\G)" +assumes f_def: "f \ \x. THE_default (d x) (\y. (x,y)\G)" assumes ex1: "\!y. (x,y)\G" shows "(x, f x)\G" by (simp only:f_def, rule THE_defaultI', rule ex1) lemma fundef_ex1_uniqueness: -assumes f_def: "f \ \x. THE_default d (\y. (x,y)\G)" +assumes f_def: "f \ \x. THE_default (d x) (\y. (x,y)\G)" assumes ex1: "\!y. (x,y)\G" assumes elm: "(x, h x)\G" shows "h x = f x" by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm) lemma fundef_ex1_iff: -assumes f_def: "f \ \x. THE_default d (\y. (x,y)\G)" +assumes f_def: "f \ \x. THE_default (d x) (\y. (x,y)\G)" assumes ex1: "\!y. (x,y)\G" shows "((x, y)\G) = (f x = y)" apply (auto simp:ex1 f_def THE_default1_equality) by (rule THE_defaultI', rule ex1) +lemma fundef_default_value: +assumes f_def: "f \ \x. THE_default (d x) (\y. (x,y)\G)" +assumes graph: "\x y. (x,y) \ G \ x \ D" +assumes "x \ D" +shows "f x = d x" +proof - + have "\(\y. (x, y) \ G)" + proof + assume "(\y. (x, y) \ G)" + with graph and `x\D` show False by blast + qed + hence "\(\!y. (x, y) \ G)" by blast + + thus ?thesis + unfolding f_def + by (rule THE_default_none) +qed + + + subsection {* Projections *} consts diff -r 24cda2c5fd40 -r d80502f0d701 src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Thu Sep 21 03:17:51 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Thu Sep 21 12:22:05 2006 +0200 @@ -214,6 +214,54 @@ val map_fundef_congs = FundefCongs.map val get_fundef_congs = FundefCongs.get + +(* Configuration management *) +datatype fundef_opt + = Sequential + | Default of string + | Preprocessor of string + +datatype fundef_config + = FundefConfig of + { + sequential: bool, + default: string, + preprocessor: string option + } + + +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE } +val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE } + +fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor}) = + FundefConfig {sequential=true, default=default, preprocessor=preprocessor } + | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor}) = + FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor } + | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor}) = + FundefConfig {sequential=sequential, default=default, preprocessor=SOME p } + + +local structure P = OuterParse and K = OuterKeyword in + +val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false + +val option_parser = (P.$$$ "sequential" >> K Sequential) + || ((P.reserved "default" |-- P.term) >> Default) + +val config_parser = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") []) + >> (fn opts => fold apply_opt opts default_config) +end + + + + + + + + + + + end diff -r 24cda2c5fd40 -r d80502f0d701 src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Thu Sep 21 03:17:51 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Thu Sep 21 12:22:05 2006 +0200 @@ -192,7 +192,7 @@ OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow) >> (fn ((target, fixes), statements) => - Toplevel.print o Toplevel.local_theory NONE (FundefPackage.add_fundef fixes statements true + Toplevel.print o Toplevel.local_theory NONE (FundefPackage.add_fundef fixes statements FundefCommon.fun_config #> by_pat_completeness_simp))); val _ = OuterSyntax.add_parsers [funP]; diff -r 24cda2c5fd40 -r d80502f0d701 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Thu Sep 21 03:17:51 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Sep 21 12:22:05 2006 +0200 @@ -11,7 +11,7 @@ sig val add_fundef : (string * string option * mixfix) list -> ((bstring * Attrib.src list) * string list) list list - -> bool + -> FundefCommon.fundef_config -> local_theory -> Proof.state @@ -34,6 +34,7 @@ open FundefCommon +(*fn (ctxt,s) => Variable.importT_terms (fst (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] [s])) ctxt;*) fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *) let val (xs, ys) = split_list ps @@ -101,14 +102,16 @@ end -fun gen_add_fundef prep_spec fixspec eqnss_flags preprocess lthy = +fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy = let - val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags preprocess lthy + val FundefConfig {sequential, default, ...} = config + + val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential 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 + FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy val afterqed = fundef_afterqed fixes spec mutual_info name prep_result in @@ -198,9 +201,9 @@ val functionP = OuterSyntax.command "function" "define general recursive functions" K.thy_goal - ((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))); + ((config_parser -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow) + >> (fn (((config, target), fixes), statements) => + Toplevel.print o local_theory_to_proof (add_fundef fixes statements config))); val terminationP = @@ -211,7 +214,7 @@ val _ = OuterSyntax.add_parsers [functionP]; val _ = OuterSyntax.add_parsers [terminationP]; -val _ = OuterSyntax.add_keywords ["sequential", "otherwise"]; (* currently unused *) +val _ = OuterSyntax.add_keywords ["sequential", "otherwise"]; end; diff -r 24cda2c5fd40 -r d80502f0d701 src/HOL/Tools/function_package/fundef_prep.ML --- a/src/HOL/Tools/function_package/fundef_prep.ML Thu Sep 21 03:17:51 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_prep.ML Thu Sep 21 12:22:05 2006 +0200 @@ -12,6 +12,7 @@ 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 @@ -419,10 +420,10 @@ -fun define_function fdefname (fname, mixfix) domT ranT G lthy = +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) $ Const ("arbitrary", ranT) $ + Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $ Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)) val ((f, (_, f_defthm)), lthy) = LocalTheory.def ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy @@ -486,11 +487,13 @@ -fun prepare_fundef defname (fname, fT, mixfix) abstract_qglrs lthy = +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 @@ -510,7 +513,7 @@ val RCss = map find_calls trees val ((G, GIntro_thms, G_elim), lthy) = define_graph (defname ^ "_graph") fvar domT ranT clauses RCss lthy - val ((f, f_defthm), lthy) = define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G lthy + val ((f, f_defthm), lthy) = 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 diff -r 24cda2c5fd40 -r d80502f0d701 src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Thu Sep 21 03:17:51 2006 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Thu Sep 21 12:22:05 2006 +0200 @@ -12,6 +12,7 @@ val prepare_fundef_mutual : ((string * typ) * mixfix) list -> term list + -> string (* default, unparsed term *) -> local_theory -> ((FundefCommon.mutual_info * string * FundefCommon.prep_result) * local_theory) @@ -42,7 +43,7 @@ fun check_head fs t = if (case t of - (Free (n, _)) => n mem fs + (Free (n, _)) => n mem (map fst fs) | _ => false) then dest_Free t else raise ERROR "Head symbol of every left hand side must be the new function." (* FIXME: Output the equation here *) @@ -54,7 +55,7 @@ (* Builds a curried clause description in abstracted form *) -fun split_def fnames geq = +fun split_def fs geq arities = let val (qs, imp) = open_all_all geq @@ -63,7 +64,7 @@ val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) val (fc, args) = strip_comb f_args - val f as (fname, _) = check_head fnames fc + val f as (fname, _) = check_head fs fc fun add_bvs t is = add_loose_bnos (t, 0, is) val rhs_only = (add_bvs rhs [] \\ fold add_bvs args []) @@ -71,8 +72,16 @@ |> map (fst o nth (rev qs)) val _ = if null rhs_only then () else raise ERROR "Variables occur on right hand side only." (* FIXME: Output vars *) + + val k = length args + + val arities' = case Symtab.lookup arities fname of + NONE => Symtab.update (fname, k) arities + | SOME i => if (i <> k) + then raise ERROR ("Function " ^ fname ^ " has different numbers of arguments in different equations") + else arities in - ((f, length args), (fname, qs, gs, args, rhs)) + ((fname, qs, gs, args, rhs), arities') end fun get_part fname = @@ -89,45 +98,38 @@ end; -fun analyze_eqs ctxt fnames eqs = +fun analyze_eqs ctxt fs eqs = let - (* FIXME: Add check for number of arguments - fun all_equal ((x as ((n:string,T), k:int))::xs) = if forall (fn ((n',_),k') => n = n' andalso k = k') xs then x - else raise ERROR ("All equations in a block must describe the same " - ^ "function and have the same number of arguments.") - *) - - val (consts, fqgars) = split_list (map (split_def fnames) eqs) + val fnames = map fst fs + val (fqgars, arities) = fold_map (split_def fs) eqs Symtab.empty - val different_consts = distinct (eq_fst (eq_fst eq_str)) consts - val cnames = map (fst o fst) different_consts - - val check_rcs = exists_subterm (fn Free (n, _) => if n mem cnames + val check_rcs = exists_subterm (fn Free (n, _) => if n mem fnames then raise ERROR "Recursive Calls not allowed in premises." else false | _ => false) val _ = forall (fn (_, _, gs, _, _) => forall check_rcs gs) fqgars - fun curried_types ((_,T), k) = + fun curried_types (fname, fT) = let - val (caTs, uaTs) = chop k (binder_types T) + val k = the_default 1 (Symtab.lookup arities fname) + val (caTs, uaTs) = chop k (binder_types fT) in - (caTs, uaTs ---> body_type T) + (caTs, uaTs ---> body_type fT) end - val (caTss, resultTs) = split_list (map curried_types different_consts) + val (caTss, resultTs) = split_list (map curried_types fs) val argTs = map (foldr1 HOLogic.mk_prodT) caTss 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 cnames) + 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 = (fsum_var_name, fsum_type) - fun define (fvar as (n, T), _) caTs pthA pthR = + fun define (fvar as (n, T)) caTs pthA pthR = let val vars = map_index (fn (i,T) => Free ("x" ^ string_of_int i, T)) caTs (* FIXME: Bind xs properly *) @@ -139,7 +141,7 @@ (MutualPart {fvar=fvar,cargTs=caTs,pthA=pthA,pthR=pthR,f_def=def,f=NONE,f_defthm=NONE}, rew) end - val (parts, rews) = split_list (map4 define different_consts caTss pthsA pthsR) + val (parts, rews) = split_list (map4 define fs caTss pthsA pthsR) fun convert_eqs (f, qs, gs, args, rhs) = let @@ -181,17 +183,13 @@ end - - - - -fun prepare_fundef_mutual fixes eqss lthy = +fun prepare_fundef_mutual fixes eqss default lthy = let - val mutual = analyze_eqs lthy (map (fst o fst) fixes) eqss + 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 lthy + FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy val (mutual', lthy'') = define_projections fixes mutual fsum lthy' in diff -r 24cda2c5fd40 -r d80502f0d701 src/HOL/Tools/function_package/pattern_split.ML --- a/src/HOL/Tools/function_package/pattern_split.ML Thu Sep 21 03:17:51 2006 +0200 +++ b/src/HOL/Tools/function_package/pattern_split.ML Thu Sep 21 12:22:05 2006 +0200 @@ -94,9 +94,6 @@ val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1 val (_, _ $ (_ $ lhs2 $ _)) = dest_all_all eq2 - val _ = print (cterm_of thy eq1) - val _ = print (cterm_of thy eq2) - val substs = pattern_subtract_subst ctx vs lhs1 lhs2 fun instantiate (vs', sigma) = @@ -105,10 +102,8 @@ in fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t end - - fun prtrm t = let val _ = print (map (cterm_of thy) t) in t end in - prtrm (map instantiate substs) + map instantiate substs end