1. Function package accepts a parameter (default "some_term"), which specifies the functions
authorkrauss
Thu Sep 21 12:22:05 2006 +0200 (2006-09-21)
changeset 20654d80502f0d701
parent 20653 24cda2c5fd40
child 20655 8c4d80e8025f
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.
src/HOL/FunDef.thy
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/function_package/mutual.ML
src/HOL/Tools/function_package/pattern_split.ML
     1.1 --- a/src/HOL/FunDef.thy	Thu Sep 21 03:17:51 2006 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Thu Sep 21 12:22:05 2006 +0200
     1.3 @@ -41,25 +41,45 @@
     1.4  
     1.5  
     1.6  lemma fundef_ex1_existence:
     1.7 -assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)"
     1.8 +assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
     1.9  assumes ex1: "\<exists>!y. (x,y)\<in>G"
    1.10  shows "(x, f x)\<in>G"
    1.11    by (simp only:f_def, rule THE_defaultI', rule ex1)
    1.12  
    1.13  lemma fundef_ex1_uniqueness:
    1.14 -assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)"
    1.15 +assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
    1.16  assumes ex1: "\<exists>!y. (x,y)\<in>G"
    1.17  assumes elm: "(x, h x)\<in>G"
    1.18  shows "h x = f x"
    1.19    by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm)
    1.20  
    1.21  lemma fundef_ex1_iff:
    1.22 -assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)"
    1.23 +assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
    1.24  assumes ex1: "\<exists>!y. (x,y)\<in>G"
    1.25  shows "((x, y)\<in>G) = (f x = y)"
    1.26    apply (auto simp:ex1 f_def THE_default1_equality)
    1.27    by (rule THE_defaultI', rule ex1)
    1.28  
    1.29 +lemma fundef_default_value:
    1.30 +assumes f_def: "f \<equiv> \<lambda>x. THE_default (d x) (\<lambda>y. (x,y)\<in>G)"
    1.31 +assumes graph: "\<And>x y. (x,y) \<in> G \<Longrightarrow> x \<in> D"
    1.32 +assumes "x \<notin> D"
    1.33 +shows "f x = d x"
    1.34 +proof -
    1.35 +  have "\<not>(\<exists>y. (x, y) \<in> G)"
    1.36 +  proof
    1.37 +    assume "(\<exists>y. (x, y) \<in> G)"
    1.38 +    with graph and `x\<notin>D` show False by blast
    1.39 +  qed
    1.40 +  hence "\<not>(\<exists>!y. (x, y) \<in> G)" by blast
    1.41 +  
    1.42 +  thus ?thesis
    1.43 +    unfolding f_def
    1.44 +    by (rule THE_default_none)
    1.45 +qed
    1.46 +
    1.47 +
    1.48 +
    1.49  
    1.50  subsection {* Projections *}
    1.51  consts
     2.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Sep 21 03:17:51 2006 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Sep 21 12:22:05 2006 +0200
     2.3 @@ -214,6 +214,54 @@
     2.4  val map_fundef_congs = FundefCongs.map 
     2.5  val get_fundef_congs = FundefCongs.get
     2.6  
     2.7 +
     2.8 +(* Configuration management *)
     2.9 +datatype fundef_opt 
    2.10 +  = Sequential
    2.11 +  | Default of string
    2.12 +  | Preprocessor of string
    2.13 +
    2.14 +datatype fundef_config
    2.15 +  = FundefConfig of
    2.16 +   {
    2.17 +    sequential: bool,
    2.18 +    default: string,
    2.19 +    preprocessor: string option
    2.20 +   }
    2.21 +
    2.22 +
    2.23 +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE }
    2.24 +val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE }
    2.25 +
    2.26 +fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor}) = 
    2.27 +    FundefConfig {sequential=true, default=default, preprocessor=preprocessor }
    2.28 +  | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor}) = 
    2.29 +    FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor }
    2.30 +  | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor}) = 
    2.31 +    FundefConfig {sequential=sequential, default=default, preprocessor=SOME p }
    2.32 +
    2.33 +    
    2.34 +local structure P = OuterParse and K = OuterKeyword in
    2.35 +
    2.36 +val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
    2.37 +
    2.38 +val option_parser = (P.$$$ "sequential" >> K Sequential)
    2.39 +               || ((P.reserved "default" |-- P.term) >> Default)
    2.40 +
    2.41 +val config_parser = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") [])
    2.42 +                      >> (fn opts => fold apply_opt opts default_config)
    2.43 +end
    2.44 +
    2.45 +
    2.46 +
    2.47 +
    2.48 +
    2.49 +
    2.50 +
    2.51 +
    2.52 +
    2.53 +
    2.54 +
    2.55  end
    2.56  
    2.57  
     3.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Thu Sep 21 03:17:51 2006 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Thu Sep 21 12:22:05 2006 +0200
     3.3 @@ -192,7 +192,7 @@
     3.4    OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
     3.5    ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
     3.6       >> (fn ((target, fixes), statements) =>
     3.7 -            Toplevel.print o Toplevel.local_theory NONE (FundefPackage.add_fundef fixes statements true 
     3.8 +            Toplevel.print o Toplevel.local_theory NONE (FundefPackage.add_fundef fixes statements FundefCommon.fun_config 
     3.9                                                                                    #> by_pat_completeness_simp)));
    3.10  
    3.11  val _ = OuterSyntax.add_parsers [funP];
     4.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Sep 21 03:17:51 2006 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Sep 21 12:22:05 2006 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4  sig
     4.5      val add_fundef :  (string * string option * mixfix) list 
     4.6                        -> ((bstring * Attrib.src list) * string list) list list
     4.7 -                      -> bool 
     4.8 +                      -> FundefCommon.fundef_config 
     4.9                        -> local_theory 
    4.10                        -> Proof.state
    4.11  
    4.12 @@ -34,6 +34,7 @@
    4.13  
    4.14  open FundefCommon
    4.15  
    4.16 +(*fn (ctxt,s) => Variable.importT_terms (fst (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] [s])) ctxt;*)
    4.17  
    4.18  fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
    4.19      let val (xs, ys) = split_list ps
    4.20 @@ -101,14 +102,16 @@
    4.21      end
    4.22  
    4.23  
    4.24 -fun gen_add_fundef prep_spec fixspec eqnss_flags preprocess lthy =
    4.25 +fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy =
    4.26      let
    4.27 -      val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags preprocess lthy
    4.28 +      val FundefConfig {sequential, default, ...} = config
    4.29 +
    4.30 +      val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy
    4.31        val t_eqns = spec
    4.32                       |> flat |> map snd |> flat (* flatten external structure *)
    4.33  
    4.34        val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) = 
    4.35 -          FundefMutual.prepare_fundef_mutual fixes t_eqns lthy
    4.36 +          FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy
    4.37  
    4.38        val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
    4.39      in
    4.40 @@ -198,9 +201,9 @@
    4.41  
    4.42  val functionP =
    4.43    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    4.44 -  ((opt_sequential -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    4.45 -     >> (fn (((sequential, target), fixes), statements) =>
    4.46 -            Toplevel.print o local_theory_to_proof (add_fundef fixes statements sequential)));
    4.47 +  ((config_parser -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    4.48 +     >> (fn (((config, target), fixes), statements) =>
    4.49 +            Toplevel.print o local_theory_to_proof (add_fundef fixes statements config)));
    4.50  
    4.51  
    4.52  val terminationP =
    4.53 @@ -211,7 +214,7 @@
    4.54  
    4.55  val _ = OuterSyntax.add_parsers [functionP];
    4.56  val _ = OuterSyntax.add_parsers [terminationP];
    4.57 -val _ = OuterSyntax.add_keywords ["sequential", "otherwise"]; (* currently unused *)
    4.58 +val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
    4.59  
    4.60  end;
    4.61  
     5.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Thu Sep 21 03:17:51 2006 +0200
     5.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Thu Sep 21 12:22:05 2006 +0200
     5.3 @@ -12,6 +12,7 @@
     5.4      val prepare_fundef : string (* defname *)
     5.5                           -> (string * typ * mixfix) (* defined symbol *)
     5.6                           -> ((string * typ) list * term list * term * term) list (* specification *)
     5.7 +                         -> string (* default_value, not parsed yet *)
     5.8                           -> local_theory
     5.9                           -> FundefCommon.prep_result * term * local_theory
    5.10  
    5.11 @@ -419,10 +420,10 @@
    5.12  
    5.13  
    5.14  
    5.15 -fun define_function fdefname (fname, mixfix) domT ranT G lthy =
    5.16 +fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
    5.17      let
    5.18        val f_def = 
    5.19 -          Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ Const ("arbitrary", ranT) $
    5.20 +          Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
    5.21                                  Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G))
    5.22            
    5.23        val ((f, (_, f_defthm)), lthy) = LocalTheory.def ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
    5.24 @@ -486,11 +487,13 @@
    5.25  
    5.26  
    5.27  
    5.28 -fun prepare_fundef defname (fname, fT, mixfix) abstract_qglrs lthy =
    5.29 +fun prepare_fundef defname (fname, fT, mixfix) abstract_qglrs default_str lthy =
    5.30      let
    5.31        val fvar = Free (fname, fT)
    5.32        val domT = domain_type fT
    5.33        val ranT = range_type fT
    5.34 +                            
    5.35 +      val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
    5.36  
    5.37        val congs = get_fundef_congs (Context.Proof lthy)
    5.38        val (globals, ctxt') = fix_globals domT ranT fvar lthy
    5.39 @@ -510,7 +513,7 @@
    5.40        val RCss = map find_calls trees
    5.41  
    5.42        val ((G, GIntro_thms, G_elim), lthy) = define_graph (defname ^ "_graph") fvar domT ranT clauses RCss lthy
    5.43 -      val ((f, f_defthm), lthy) = define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G lthy
    5.44 +      val ((f, f_defthm), lthy) = define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default lthy
    5.45  
    5.46        val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
    5.47        val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
     6.1 --- a/src/HOL/Tools/function_package/mutual.ML	Thu Sep 21 03:17:51 2006 +0200
     6.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Thu Sep 21 12:22:05 2006 +0200
     6.3 @@ -12,6 +12,7 @@
     6.4    
     6.5    val prepare_fundef_mutual : ((string * typ) * mixfix) list 
     6.6                                -> term list 
     6.7 +                              -> string (* default, unparsed term *)
     6.8                                -> local_theory 
     6.9                                -> ((FundefCommon.mutual_info * string * FundefCommon.prep_result) * local_theory)
    6.10  
    6.11 @@ -42,7 +43,7 @@
    6.12  
    6.13  fun check_head fs t =
    6.14      if (case t of 
    6.15 -          (Free (n, _)) => n mem fs
    6.16 +          (Free (n, _)) => n mem (map fst fs)
    6.17          | _ => false)
    6.18      then dest_Free t
    6.19      else raise ERROR "Head symbol of every left hand side must be the new function." (* FIXME: Output the equation here *)
    6.20 @@ -54,7 +55,7 @@
    6.21  
    6.22  
    6.23  (* Builds a curried clause description in abstracted form *)
    6.24 -fun split_def fnames geq =
    6.25 +fun split_def fs geq arities =
    6.26      let
    6.27        val (qs, imp) = open_all_all geq
    6.28  
    6.29 @@ -63,7 +64,7 @@
    6.30  
    6.31        val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
    6.32        val (fc, args) = strip_comb f_args
    6.33 -      val f as (fname, _) = check_head fnames fc
    6.34 +      val f as (fname, _) = check_head fs fc
    6.35  
    6.36        fun add_bvs t is = add_loose_bnos (t, 0, is)
    6.37        val rhs_only = (add_bvs rhs [] \\ fold add_bvs args [])
    6.38 @@ -71,8 +72,16 @@
    6.39                          |> map (fst o nth (rev qs))
    6.40        val _ = if null rhs_only then () 
    6.41  	      else raise ERROR "Variables occur on right hand side only." (* FIXME: Output vars *)
    6.42 +
    6.43 +      val k = length args
    6.44 +
    6.45 +      val arities' = case Symtab.lookup arities fname of
    6.46 +                   NONE => Symtab.update (fname, k) arities
    6.47 +                 | SOME i => if (i <> k) 
    6.48 +                             then raise ERROR ("Function " ^ fname ^ " has different numbers of arguments in different equations")
    6.49 +                             else arities
    6.50      in
    6.51 -	((f, length args), (fname, qs, gs, args, rhs))
    6.52 +	((fname, qs, gs, args, rhs), arities')
    6.53      end
    6.54  
    6.55  fun get_part fname =
    6.56 @@ -89,45 +98,38 @@
    6.57      end;
    6.58  
    6.59  
    6.60 -fun analyze_eqs ctxt fnames eqs =
    6.61 +fun analyze_eqs ctxt fs eqs =
    6.62      let
    6.63 -      (* FIXME: Add check for number of arguments
    6.64 -	fun all_equal ((x as ((n:string,T), k:int))::xs) = if forall (fn ((n',_),k') => n = n' andalso k = k') xs then x
    6.65 -							   else raise ERROR ("All equations in a block must describe the same "
    6.66 -									     ^ "function and have the same number of arguments.")
    6.67 -       *)
    6.68 -								      
    6.69 -        val (consts, fqgars) = split_list (map (split_def fnames) eqs)
    6.70 +        val fnames = map fst fs 
    6.71 +        val (fqgars, arities) = fold_map (split_def fs) eqs Symtab.empty
    6.72  
    6.73 -        val different_consts = distinct (eq_fst (eq_fst eq_str)) consts
    6.74 -	val cnames = map (fst o fst) different_consts
    6.75 -
    6.76 -	val check_rcs = exists_subterm (fn Free (n, _) => if n mem cnames 
    6.77 +	val check_rcs = exists_subterm (fn Free (n, _) => if n mem fnames
    6.78  						          then raise ERROR "Recursive Calls not allowed in premises." else false
    6.79                                           | _ => false)
    6.80                          
    6.81  	val _ = forall (fn (_, _, gs, _, _) => forall check_rcs gs) fqgars
    6.82  
    6.83 -	fun curried_types ((_,T), k) =
    6.84 +	fun curried_types (fname, fT) =
    6.85  	    let
    6.86 -		val (caTs, uaTs) = chop k (binder_types T)
    6.87 +              val k = the_default 1 (Symtab.lookup arities fname)
    6.88 +	      val (caTs, uaTs) = chop k (binder_types fT)
    6.89  	    in 
    6.90 -		(caTs, uaTs ---> body_type T)
    6.91 +		(caTs, uaTs ---> body_type fT)
    6.92  	    end
    6.93  
    6.94 -	val (caTss, resultTs) = split_list (map curried_types different_consts)
    6.95 +	val (caTss, resultTs) = split_list (map curried_types fs)
    6.96  	val argTs = map (foldr1 HOLogic.mk_prodT) caTss
    6.97  
    6.98  	val (RST,streeR, pthsR) = SumTools.mk_tree_distinct resultTs
    6.99  	val (ST, streeA, pthsA) = SumTools.mk_tree argTs
   6.100  
   6.101 -	val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name cnames)
   6.102 +	val def_name = foldr1 (fn (a,b) => a ^ "_" ^ b) (map Sign.base_name fnames)
   6.103  	val fsum_type = ST --> RST
   6.104  
   6.105          val ([fsum_var_name], _) = Variable.add_fixes [ def_name ^ "_sum" ] ctxt
   6.106          val fsum_var = (fsum_var_name, fsum_type)
   6.107  
   6.108 -	fun define (fvar as (n, T), _) caTs pthA pthR = 
   6.109 +	fun define (fvar as (n, T)) caTs pthA pthR = 
   6.110  	    let 
   6.111  		val vars = map_index (fn (i,T) => Free ("x" ^ string_of_int i, T)) caTs (* FIXME: Bind xs properly *)
   6.112  
   6.113 @@ -139,7 +141,7 @@
   6.114  		(MutualPart {fvar=fvar,cargTs=caTs,pthA=pthA,pthR=pthR,f_def=def,f=NONE,f_defthm=NONE}, rew)
   6.115  	    end
   6.116  
   6.117 -	val (parts, rews) = split_list (map4 define different_consts caTss pthsA pthsR)
   6.118 +	val (parts, rews) = split_list (map4 define fs caTss pthsA pthsR)
   6.119  
   6.120          fun convert_eqs (f, qs, gs, args, rhs) =
   6.121              let
   6.122 @@ -181,17 +183,13 @@
   6.123      end
   6.124  
   6.125  
   6.126 -
   6.127 -  
   6.128 -
   6.129 -
   6.130 -fun prepare_fundef_mutual fixes eqss lthy =
   6.131 +fun prepare_fundef_mutual fixes eqss default lthy =
   6.132      let 
   6.133 -	val mutual = analyze_eqs lthy (map (fst o fst) fixes) eqss
   6.134 +	val mutual = analyze_eqs lthy (map fst fixes) eqss
   6.135  	val Mutual {defname, fsum_var=(n, T), qglrs, ...} = mutual
   6.136  
   6.137          val (prep_result, fsum, lthy') =
   6.138 -            FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs lthy
   6.139 +            FundefPrep.prepare_fundef defname (n, T, NoSyn) qglrs default lthy
   6.140  
   6.141          val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
   6.142      in
     7.1 --- a/src/HOL/Tools/function_package/pattern_split.ML	Thu Sep 21 03:17:51 2006 +0200
     7.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Thu Sep 21 12:22:05 2006 +0200
     7.3 @@ -94,9 +94,6 @@
     7.4        val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
     7.5        val (_,  _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
     7.6  
     7.7 -      val _ = print (cterm_of thy eq1)
     7.8 -      val _ = print (cterm_of thy eq2)
     7.9 -
    7.10        val substs = pattern_subtract_subst ctx vs lhs1 lhs2
    7.11  
    7.12        fun instantiate (vs', sigma) =
    7.13 @@ -105,10 +102,8 @@
    7.14            in
    7.15              fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t
    7.16            end
    7.17 -
    7.18 -      fun prtrm t = let val _ = print (map (cterm_of thy) t) in t end
    7.19      in
    7.20 -      prtrm (map instantiate substs)
    7.21 +      map instantiate substs
    7.22      end
    7.23  
    7.24