src/HOL/Tools/function_package/fundef_package.ML
changeset 20523 36a59e5d0039
parent 20363 f34c5dbe74d5
child 20638 241792a4634e
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 13 00:38:38 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 13 12:05:50 2006 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  (*  Title:      HOL/Tools/function_package/fundef_package.ML
     1.6      ID:         $Id$
     1.7      Author:     Alexander Krauss, TU Muenchen
     1.8 @@ -10,7 +9,17 @@
     1.9  
    1.10  signature FUNDEF_PACKAGE =
    1.11  sig
    1.12 -    val add_fundef : ((bstring * (Attrib.src list * bool)) * string) list list -> bool -> theory -> Proof.state (* Need an _i variant *)
    1.13 +    val add_fundef :  (string * string option * mixfix) list 
    1.14 +                      -> ((bstring * Attrib.src list) * string list) list list
    1.15 +                      -> bool 
    1.16 +                      -> local_theory 
    1.17 +                      -> Proof.state
    1.18 +
    1.19 +    val add_fundef_i:  (string * typ option * mixfix) list 
    1.20 +                       -> ((bstring * Attrib.src list) * term list) list list
    1.21 +                       -> bool 
    1.22 +                       -> local_theory 
    1.23 +                       -> Proof.state
    1.24  
    1.25      val cong_add: attribute
    1.26      val cong_del: attribute
    1.27 @@ -20,167 +29,136 @@
    1.28  end
    1.29  
    1.30  
    1.31 -structure FundefPackage : FUNDEF_PACKAGE =
    1.32 +structure FundefPackage  =
    1.33  struct
    1.34  
    1.35  open FundefCommon
    1.36  
    1.37  
    1.38 -fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy =
    1.39 -    let
    1.40 -      val psimpss = Library.unflat (map snd spec_part) psimps
    1.41 -      val (names, attss) = split_list (map fst spec_part)
    1.42 +fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
    1.43 +    let val (xs, ys) = split_list ps
    1.44 +    in xs ~~ f ys end
    1.45  
    1.46 -      val thy = thy |> Theory.add_path f_name
    1.47 +fun restore_spec_structure reps spec =
    1.48 +    (burrow o burrow_snd o burrow o K) reps spec
    1.49  
    1.50 -      val thy = thy |> Theory.add_path label
    1.51 -      val spsimpss = map (map standard) psimpss (* FIXME *)
    1.52 -      val add_list = (names ~~ spsimpss) ~~ attss
    1.53 -      val (_, thy) = PureThy.add_thmss add_list thy
    1.54 -      val thy = thy |> Theory.parent_path
    1.55 -
    1.56 -      val (_, thy) = PureThy.add_thmss [((label, flat spsimpss), Simplifier.simp_add :: moreatts)] thy
    1.57 -      val thy = thy |> Theory.parent_path
    1.58 +fun with_local_path path f lthy =
    1.59 +    let 
    1.60 +      val restore = Theory.restore_naming (ProofContext.theory_of lthy)
    1.61      in
    1.62 -      thy
    1.63 +      lthy
    1.64 +        |> LocalTheory.theory (Theory.add_path path)
    1.65 +        |> f
    1.66 +        |> LocalTheory.theory restore
    1.67      end
    1.68  
    1.69 -
    1.70 -
    1.71 -
    1.72 -
    1.73 -
    1.74 -fun fundef_afterqed congs mutual_info name data spec [[result]] thy =
    1.75 +fun add_simps label moreatts mutual_info fixes psimps spec lthy =
    1.76      let
    1.77 -        val fundef_data = FundefMutual.mk_partial_rules_mutual thy mutual_info data result
    1.78 -        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    1.79 -        val Mutual {parts, ...} = mutual_info
    1.80 +      val fnames = map (fst o fst) fixes
    1.81 +      val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames psimps
    1.82  
    1.83 -        val Prep {names = Names {acc_R=accR, ...}, ...} = data
    1.84 -        val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    1.85 -        val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    1.86 -
    1.87 -        val thy = fold2 (add_simps "psimps" []) (parts ~~ psimps) spec thy
    1.88 -
    1.89 -        val casenames = flat (map (map (fst o fst)) spec)
    1.90 -
    1.91 -        val thy = thy |> Theory.add_path name
    1.92 -        val (_, thy) = PureThy.add_thms [(("cases", cases), [RuleCases.case_names casenames])] thy
    1.93 -        val (_, thy) = PureThy.add_thmss [(("domintros", domintros), [])] thy
    1.94 -        val (_, thy) = PureThy.add_thms [(("termination", standard termination), [])] thy
    1.95 -        val (_,thy) = PureThy.add_thmss [(("pinduct", map standard simple_pinducts), [RuleCases.case_names casenames, InductAttrib.induct_set ""])] thy
    1.96 -        val thy = thy |> Theory.parent_path
    1.97 +      fun add_for_f fname psimps =
    1.98 +          with_local_path fname
    1.99 +                          (LocalTheory.note ((label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd)
   1.100      in
   1.101 -      add_fundef_data name (fundef_data, mutual_info, spec) thy
   1.102 -    end
   1.103 -
   1.104 -fun gen_add_fundef prep_att eqns_attss (preprocess : bool) thy =
   1.105 -    let
   1.106 -      fun prep_eqns neqs =
   1.107 -          neqs
   1.108 -            |> map (apsnd (Sign.read_prop thy))
   1.109 -            |> map (apfst (apsnd (apfst (map (prep_att thy)))))
   1.110 -            |> FundefSplit.split_some_equations (ProofContext.init thy)
   1.111 -
   1.112 -      val spec = map prep_eqns eqns_attss
   1.113 -      val t_eqnss = map (flat o map snd) spec
   1.114 -
   1.115 -      val congs = get_fundef_congs (Context.Theory thy)
   1.116 -
   1.117 -      val (mutual_info, name, (data, thy)) = FundefMutual.prepare_fundef_mutual congs t_eqnss thy
   1.118 -      val Prep {goal, goalI, ...} = data
   1.119 -    in
   1.120 -      thy |> ProofContext.init
   1.121 -          |> Proof.theorem_i PureThy.internalK NONE
   1.122 -              (ProofContext.theory o fundef_afterqed congs mutual_info name data spec) NONE ("", [])
   1.123 -              [(("", []), [(goal, [])])]
   1.124 -          |> Proof.refine (Method.primitive_text (fn _ => goalI))
   1.125 -          |> Seq.hd
   1.126 +      lthy
   1.127 +        |> fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) |> snd
   1.128 +        |> fold2 add_for_f fnames psimps_by_f
   1.129      end
   1.130  
   1.131  
   1.132 -fun total_termination_afterqed name (Mutual {parts, ...}) thmss thy =
   1.133 +fun fundef_afterqed fixes spec mutual_info defname data [[result]] lthy =
   1.134 +    let
   1.135 +        val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
   1.136 +        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
   1.137 +    in
   1.138 +      lthy
   1.139 +        |> add_simps "psimps" [] mutual_info fixes psimps spec
   1.140 +        |> with_local_path defname
   1.141 +                  (LocalTheory.note (("domintros", []), domintros) #> snd
   1.142 +                   #> LocalTheory.note (("termination", []), [termination]) #> snd
   1.143 +                   #> LocalTheory.note (("cases", []), [cases]) #> snd
   1.144 +                   #> LocalTheory.note (("pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) #> snd)
   1.145 +        |> LocalTheory.theory (Context.theory_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))))
   1.146 +    end (* FIXME: Add cases for induct and cases thm *)
   1.147 +
   1.148 +
   1.149 +
   1.150 +fun prep_with_flags prep fixspec eqnss_flags global_flag lthy =
   1.151      let
   1.152 -        val totality = hd (hd thmss)
   1.153 +      val eqnss = map (map (apsnd (map fst))) eqnss_flags
   1.154 +      val flags = map (map (map (fn (_, f) => global_flag orelse f) o snd)) eqnss_flags
   1.155 +
   1.156 +      val ((fixes, _), ctxt') = prep fixspec [] lthy
   1.157 +      val spec = map (fn eqns => snd (fst (prep [] eqns ctxt'))) eqnss
   1.158 +                     |> map (map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)))) (* Add quantifiers *)
   1.159 +                     |> map2 (map2 (fn fs => fn (r, thms) => (r, fs ~~ thms))) flags
   1.160 +                     |> (burrow o burrow_snd o burrow) 
   1.161 +                          (FundefSplit.split_some_equations lthy)
   1.162 +                     |> map (map (apsnd flat))
   1.163 +    in
   1.164 +      ((fixes, spec), ctxt')
   1.165 +    end
   1.166 +
   1.167  
   1.168 -        val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
   1.169 -          = the (get_fundef_data name thy)
   1.170 +fun gen_add_fundef prep_spec fixspec eqnss_flags preprocess lthy =
   1.171 +    let
   1.172 +      val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags preprocess lthy
   1.173 +      val t_eqns = spec
   1.174 +                     |> flat |> map snd |> flat (* flatten external structure *)
   1.175 +
   1.176 +      val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) = 
   1.177 +          FundefMutual.prepare_fundef_mutual fixes t_eqns lthy
   1.178 +
   1.179 +      val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
   1.180 +    in
   1.181 +        lthy
   1.182 +          |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
   1.183 +          |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd
   1.184 +    end
   1.185 +
   1.186 +
   1.187 +fun total_termination_afterqed defname data [[totality]] lthy =
   1.188 +    let
   1.189 +        val (FundefMResult {psimps, simple_pinducts, ... }, mutual_info, (fixes, stmts)) = data
   1.190  
   1.191          val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
   1.192  
   1.193 -        val tsimps = map (map remove_domain_condition) psimps
   1.194 +        val tsimps = map remove_domain_condition psimps
   1.195          val tinduct = map remove_domain_condition simple_pinducts
   1.196  
   1.197 -        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps)
   1.198 -        val allatts = if has_guards then [] else [RecfunCodegen.add NONE]
   1.199 -
   1.200 -        val thy = fold2 (add_simps "simps" allatts) (parts ~~ tsimps) spec thy
   1.201 -
   1.202 -        val thy = Theory.add_path name thy
   1.203 -
   1.204 -        val (_, thy) = PureThy.add_thmss [(("induct", map standard tinduct), [])] thy
   1.205 -        val thy = Theory.parent_path thy
   1.206 +        (* FIXME: How to generate code from (possibly) local contexts 
   1.207 +        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
   1.208 +        val allatts = if has_guards then [] else [Attrib.internal (RecfunCodegen.add NONE)]
   1.209 +        *)
   1.210      in
   1.211 -        thy
   1.212 -    end
   1.213 -
   1.214 -(*
   1.215 -fun mk_partial_rules name D_name D domT idomT thmss thy =
   1.216 -    let
   1.217 -        val [subs, dcl] = (hd thmss)
   1.218 -
   1.219 -        val {f_const, f_curried_const, G_const, R_const, G_elims, completeness, f_simps, names_attrs, subset_induct, ... }
   1.220 -          = the (Symtab.lookup (FundefData.get thy) name)
   1.221 -
   1.222 -        val D_implies_dom = subs COMP (instantiate' [SOME (ctyp_of thy idomT)]
   1.223 -                                                    [SOME (cterm_of thy D)]
   1.224 -                                                    subsetD)
   1.225 -
   1.226 -        val D_simps = map (curry op RS D_implies_dom) f_simps
   1.227 -
   1.228 -        val D_induct = subset_induct
   1.229 -                           |> cterm_instantiate [(cterm_of thy (Var (("D",0), fastype_of D)) ,cterm_of thy D)]
   1.230 -                           |> curry op COMP subs
   1.231 -                           |> curry op COMP (dcl |> forall_intr (cterm_of thy (Var (("z",0), idomT)))
   1.232 -                                                 |> forall_intr (cterm_of thy (Var (("x",0), idomT))))
   1.233 -
   1.234 -        val ([tinduct'], thy2) = PureThy.add_thms [((name ^ "_" ^ D_name ^ "_induct", D_induct), [])] thy
   1.235 -        val ([tsimps'], thy3) = PureThy.add_thmss [((name ^ "_" ^ D_name ^ "_simps", D_simps), [])] thy2
   1.236 -    in
   1.237 -        thy3
   1.238 -    end
   1.239 -*)
   1.240 -
   1.241 -
   1.242 -fun fundef_setup_termination_proof name NONE thy =
   1.243 -    let
   1.244 -        val name = if name = "" then get_last_fundef thy else name
   1.245 -        val data = the (get_fundef_data name thy)
   1.246 -                   handle Option.Option => raise ERROR ("No such function definition: " ^ name)
   1.247 -
   1.248 -        val (res as FundefMResult {termination, ...}, mutual, _) = data
   1.249 -        val goal = FundefTermination.mk_total_termination_goal data
   1.250 -    in
   1.251 -        thy |> ProofContext.init
   1.252 -            |> ProofContext.note_thmss_i [(("termination",
   1.253 -                                            [ContextRules.intro_query NONE]), [([standard termination], [])])] |> snd
   1.254 -            |> Proof.theorem_i PureThy.internalK NONE
   1.255 -              (ProofContext.theory o total_termination_afterqed name mutual) NONE ("", [])
   1.256 -              [(("", []), [(goal, [])])]
   1.257 -    end
   1.258 -  | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
   1.259 -    let
   1.260 -        val name = if name = "" then get_last_fundef thy else name
   1.261 -        val data = the (get_fundef_data name thy)
   1.262 -        val (subs, dcl) = FundefTermination.mk_partial_termination_goal thy data dom
   1.263 -    in
   1.264 -        thy |> ProofContext.init
   1.265 -            |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
   1.266 -            [(("", []), [(subs, []), (dcl, [])])]
   1.267 +        lthy
   1.268 +          |> add_simps "simps" [] mutual_info fixes tsimps stmts
   1.269 +          |> with_local_path defname
   1.270 +                (LocalTheory.note (("induct", [Attrib.internal (InductAttrib.induct_set "")]), tinduct) #> snd)
   1.271      end
   1.272  
   1.273  
   1.274 -val add_fundef = gen_add_fundef Attrib.attribute
   1.275 +fun fundef_setup_termination_proof name_opt lthy =
   1.276 +    let
   1.277 +        val name = the_default (get_last_fundef (Context.Proof lthy)) name_opt
   1.278 +        val data = the (get_fundef_data name (Context.Proof lthy))
   1.279 +                   handle Option.Option => raise ERROR ("No such function definition: " ^ name)
   1.280 +
   1.281 +        val (res as FundefMResult {termination, ...}, _, _) = data
   1.282 +        val goal = FundefTermination.mk_total_termination_goal data
   1.283 +    in
   1.284 +      lthy 
   1.285 +        |> ProofContext.note_thmss_i [(("termination",
   1.286 +                                 [ContextRules.intro_query NONE]), [(ProofContext.export_standard lthy lthy [termination], [])])] |> snd
   1.287 +        |> Proof.theorem_i PureThy.internalK NONE
   1.288 +                           (total_termination_afterqed name data) NONE ("", [])
   1.289 +                           [(("", []), [(goal, [])])]
   1.290 +    end
   1.291 +
   1.292 +
   1.293 +val add_fundef = gen_add_fundef Specification.read_specification
   1.294 +val add_fundef_i = gen_add_fundef Specification.cert_specification
   1.295  
   1.296  
   1.297  
   1.298 @@ -206,39 +184,34 @@
   1.299  
   1.300  
   1.301  
   1.302 -val star = Scan.one (fn t => (OuterLex.val_of t = "*"));
   1.303 +fun or_list1 s = P.enum1 "|" s
   1.304 +
   1.305 +val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
   1.306 +
   1.307 +val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
   1.308 +val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
   1.309 +val statements_ow = or_list1 statement_ow
   1.310  
   1.311  
   1.312 -val attribs_with_star = P.$$$ "[" |-- P.!!! ((P.list (star >> K NONE || P.attrib >> SOME))
   1.313 -                                               >> (fn x => (map_filter I x, exists is_none x)))
   1.314 -                              --| P.$$$ "]";
   1.315 -
   1.316 -val opt_attribs_with_star = Scan.optional attribs_with_star ([], false);
   1.317 -
   1.318 -val opt_thm_name_star =
   1.319 -  Scan.optional ((P.name -- opt_attribs_with_star || (attribs_with_star >> pair "")) --| P.$$$ ":") ("", ([], false));
   1.320 -
   1.321 -
   1.322 -val function_decl =
   1.323 -    Scan.repeat1 (opt_thm_name_star -- P.prop);
   1.324 +fun local_theory_to_proof f = 
   1.325 +    Toplevel.theory_to_proof (f o LocalTheory.init NONE)
   1.326  
   1.327  val functionP =
   1.328    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   1.329 -  (((Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "sequential" -- P.$$$ ")") >> K true) false) --
   1.330 -  P.and_list1 function_decl) >> (fn (prepr, eqnss) =>
   1.331 -                                    Toplevel.print o Toplevel.theory_to_proof (add_fundef eqnss prepr)));
   1.332 +  ((opt_sequential -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
   1.333 +     >> (fn (((sequential, target), fixes), statements) =>
   1.334 +            Toplevel.print o local_theory_to_proof (add_fundef fixes statements sequential)));
   1.335 +
   1.336  
   1.337  val terminationP =
   1.338    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
   1.339 -  ((Scan.optional P.name "" -- Scan.option (P.$$$ "(" |-- Scan.optional (P.name --| P.$$$ ":") "dom" -- P.term --| P.$$$ ")"))
   1.340 -       >> (fn (name,dom) =>
   1.341 -              Toplevel.print o Toplevel.theory_to_proof (fundef_setup_termination_proof name dom)));
   1.342 +  (Scan.option P.name 
   1.343 +    >> (fn name => Toplevel.print o local_theory_to_proof (fundef_setup_termination_proof name)));
   1.344  
   1.345 -val _ = OuterSyntax.add_keywords ["sequential", "otherwise"];
   1.346  
   1.347  val _ = OuterSyntax.add_parsers [functionP];
   1.348  val _ = OuterSyntax.add_parsers [terminationP];
   1.349 -
   1.350 +val _ = OuterSyntax.add_keywords ["sequential", "otherwise"]; (* currently unused *)
   1.351  
   1.352  end;
   1.353