src/HOL/Tools/Function/function.ML
author wenzelm
Sat Mar 22 18:19:57 2014 +0100 (2014-03-22)
changeset 56254 a2dd9200854d
parent 55404 5cb95b79a51f
child 56932 11a4001b06c6
permissions -rw-r--r--
more antiquotations;
     1 (*  Title:      HOL/Tools/Function/function.ML
     2     Author:     Alexander Krauss, TU Muenchen
     3 
     4 Main entry points to the function package.
     5 *)
     6 
     7 signature FUNCTION =
     8 sig
     9   include FUNCTION_DATA
    10 
    11   val add_function: (binding * typ option * mixfix) list ->
    12     (Attrib.binding * term) list -> Function_Common.function_config ->
    13     (Proof.context -> tactic) -> local_theory -> info * local_theory
    14 
    15   val add_function_cmd: (binding * string option * mixfix) list ->
    16     (Attrib.binding * string) list -> Function_Common.function_config ->
    17     (Proof.context -> tactic) -> bool -> local_theory -> info * local_theory
    18 
    19   val function: (binding * typ option * mixfix) list ->
    20     (Attrib.binding * term) list -> Function_Common.function_config ->
    21     local_theory -> Proof.state
    22 
    23   val function_cmd: (binding * string option * mixfix) list ->
    24     (Attrib.binding * string) list -> Function_Common.function_config ->
    25     bool -> local_theory -> Proof.state
    26 
    27   val prove_termination: term option -> tactic -> local_theory ->
    28     info * local_theory
    29   val prove_termination_cmd: string option -> tactic -> local_theory ->
    30     info * local_theory
    31 
    32   val termination : term option -> local_theory -> Proof.state
    33   val termination_cmd : string option -> local_theory -> Proof.state
    34 
    35   val setup : theory -> theory
    36   val get_congs : Proof.context -> thm list
    37 
    38   val get_info : Proof.context -> term -> info
    39 end
    40 
    41 
    42 structure Function : FUNCTION =
    43 struct
    44 
    45 open Function_Lib
    46 open Function_Common
    47 
    48 val simp_attribs =
    49   @{attributes [simp, nitpick_simp]} @ [Attrib.internal (K Code.add_default_eqn_attribute)]
    50 
    51 val psimp_attribs =
    52   @{attributes [nitpick_psimp]}
    53 
    54 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
    55 
    56 fun note_qualified suffix attrs (fname, thms) =
    57   Local_Theory.note ((Binding.qualify true fname (Binding.name suffix),
    58     map (Attrib.internal o K) attrs), thms)
    59   #> apfst snd
    60 
    61 fun add_simps fnames post sort extra_qualify label mod_binding moreatts
    62   simps lthy =
    63   let
    64     val spec = post simps
    65       |> map (apfst (apsnd (fn ats => moreatts @ ats)))
    66       |> map (apfst (apfst extra_qualify))
    67 
    68     val (saved_spec_simps, lthy) =
    69       fold_map Local_Theory.note spec lthy
    70 
    71     val saved_simps = maps snd saved_spec_simps
    72     val simps_by_f = sort saved_simps
    73 
    74     fun add_for_f fname simps =
    75       Local_Theory.note
    76         ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
    77       #> snd
    78   in
    79     (saved_simps, fold2 add_for_f fnames simps_by_f lthy)
    80   end
    81 
    82 fun prepare_function do_print prep default_constraint fixspec eqns config lthy =
    83   let
    84     val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
    85     val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
    86     val fixes = map (apfst (apfst Binding.name_of)) fixes0;
    87     val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
    88     val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
    89 
    90     val defname = mk_defname fixes
    91     val FunctionConfig {partials, default, ...} = config
    92     val _ =
    93       if is_some default
    94       then legacy_feature "\"function (default)\" -- use 'partial_function' instead"
    95       else ()
    96 
    97     val ((goal_state, cont), lthy') =
    98       Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
    99 
   100     fun afterqed [[proof]] lthy =
   101       let
   102         val result = cont (Thm.close_derivation proof)
   103         val FunctionResult {fs, R, dom, psimps, simple_pinducts,
   104                 termination, domintros, cases, ...} = result
   105 
   106         val pelims = Function_Elims.mk_partial_elim_rules lthy result
   107 
   108         val fnames = map (fst o fst) fixes
   109         fun qualify n = Binding.name n
   110           |> Binding.qualify true defname
   111         val conceal_partial = if partials then I else Binding.conceal
   112 
   113         val addsmps = add_simps fnames post sort_cont
   114 
   115         val (((((psimps', [pinducts']), [termination']), cases'), pelims'), lthy) =
   116           lthy
   117           |> addsmps (conceal_partial o Binding.qualify false "partial")
   118                "psimps" conceal_partial psimp_attribs psimps
   119           ||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []),
   120                 simple_pinducts |> map (fn th => ([th],
   121                  [Attrib.internal (K (Rule_Cases.case_names cnames)),
   122                   Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
   123                   Attrib.internal (K (Induct.induct_pred ""))])))]
   124           ||>> (apfst snd o Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]))
   125           ||>> fold_map (note_qualified "cases" [Rule_Cases.case_names cnames]) (fnames ~~ map single cases) (* TODO: case names *)
   126           ||>> fold_map (note_qualified "pelims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ pelims)
   127           ||> (case domintros of NONE => I | SOME thms =>
   128                    Local_Theory.note ((qualify "domintros", []), thms) #> snd)
   129 
   130         val info = { add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
   131           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
   132           fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
   133           pelims=pelims',elims=NONE}
   134 
   135         val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
   136       in
   137         (info,
   138          lthy |> Local_Theory.declaration {syntax = false, pervasive = false}
   139           (add_function_data o transform_function_data info))
   140       end
   141   in
   142     ((goal_state, afterqed), lthy')
   143   end
   144 
   145 fun gen_add_function do_print prep default_constraint fixspec eqns config tac lthy =
   146   let
   147     val ((goal_state, afterqed), lthy') =
   148       prepare_function do_print prep default_constraint fixspec eqns config lthy
   149     val pattern_thm =
   150       case SINGLE (tac lthy') goal_state of
   151         NONE => error "pattern completeness and compatibility proof failed"
   152       | SOME st => Goal.finish lthy' st
   153   in
   154     lthy'
   155     |> afterqed [[pattern_thm]]
   156   end
   157 
   158 val add_function =
   159   gen_add_function false Specification.check_spec (Type_Infer.anyT @{sort type})
   160 fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec "_::type" a b c d
   161 
   162 fun gen_function do_print prep default_constraint fixspec eqns config lthy =
   163   let
   164     val ((goal_state, afterqed), lthy') =
   165       prepare_function do_print prep default_constraint fixspec eqns config lthy
   166   in
   167     lthy'
   168     |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
   169     |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
   170   end
   171 
   172 val function =
   173   gen_function false Specification.check_spec (Type_Infer.anyT @{sort type})
   174 fun function_cmd a b c int = gen_function int Specification.read_spec "_::type" a b c
   175 
   176 fun prepare_termination_proof prep_term raw_term_opt lthy =
   177   let
   178     val term_opt = Option.map (prep_term lthy) raw_term_opt
   179     val info =
   180       (case term_opt of
   181         SOME t =>
   182           (case import_function_data t lthy of
   183             SOME info => info
   184           | NONE => error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
   185       | NONE =>
   186           (case import_last_function lthy of
   187             SOME info => info
   188           | NONE => error "Not a function"))
   189 
   190     val { termination, fs, R, add_simps, case_names, psimps,
   191       pinducts, defname, fnames, cases, dom, pelims, ...} = info
   192     val domT = domain_type (fastype_of R)
   193     val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
   194     fun afterqed [[totality]] lthy =
   195       let
   196         val totality = Thm.close_derivation totality
   197         val remove_domain_condition =
   198           full_simplify (put_simpset HOL_basic_ss lthy
   199             addsimps [totality, @{thm True_implies_equals}])
   200         val tsimps = map remove_domain_condition psimps
   201         val tinduct = map remove_domain_condition pinducts
   202         val telims = map (map remove_domain_condition) pelims
   203 
   204         fun qualify n = Binding.name n
   205           |> Binding.qualify true defname
   206 
   207       in
   208         lthy
   209         |> add_simps I "simps" I simp_attribs tsimps
   210         ||>> Local_Theory.note
   211            ((qualify "induct",
   212              [Attrib.internal (K (Rule_Cases.case_names case_names))]),
   213             tinduct)
   214         ||>> fold_map (note_qualified "elims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ telims)
   215         |-> (fn ((simps,(_,inducts)), elims) => fn lthy =>
   216           let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps,
   217             case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
   218             simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases, pelims=pelims, elims=SOME elims}
   219           in
   220             (info',
   221              lthy
   222              |> Local_Theory.declaration {syntax = false, pervasive = false}
   223                (add_function_data o transform_function_data info')
   224              |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
   225           end)
   226       end
   227   in
   228     (goal, afterqed, termination)
   229   end
   230 
   231 fun gen_prove_termination prep_term raw_term_opt tac lthy =
   232   let
   233     val (goal, afterqed, termination) =
   234       prepare_termination_proof prep_term raw_term_opt lthy
   235 
   236     val totality = Goal.prove lthy [] [] goal (K tac)
   237   in
   238     afterqed [[totality]] lthy
   239 end
   240 
   241 val prove_termination = gen_prove_termination Syntax.check_term
   242 val prove_termination_cmd = gen_prove_termination Syntax.read_term
   243 
   244 fun gen_termination prep_term raw_term_opt lthy =
   245   let
   246     val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy
   247   in
   248     lthy
   249     |> Proof_Context.note_thmss ""
   250        [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
   251     |> Proof_Context.note_thmss ""
   252        [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
   253     |> Proof_Context.note_thmss ""
   254        [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
   255          [([Goal.norm_result lthy termination], [])])] |> snd
   256     |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
   257   end
   258 
   259 val termination = gen_termination Syntax.check_term
   260 val termination_cmd = gen_termination Syntax.read_term
   261 
   262 
   263 (* Datatype hook to declare datatype congs as "function_congs" *)
   264 
   265 
   266 fun add_case_cong n thy =
   267   let
   268     val cong = #case_cong (Datatype_Data.the_info thy n)
   269       |> safe_mk_meta_eq
   270   in
   271     Context.theory_map
   272       (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
   273   end
   274 
   275 val setup_case_cong = Datatype_Data.interpretation (K (fold add_case_cong))
   276 
   277 
   278 (* setup *)
   279 
   280 val setup =
   281   setup_case_cong
   282   #> Function_Common.Termination_Simps.setup
   283 
   284 val get_congs = Function_Ctx_Tree.get_function_congs
   285 
   286 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
   287   |> the_single |> snd
   288 
   289 
   290 (* outer syntax *)
   291 
   292 val _ =
   293   Outer_Syntax.local_theory_to_proof' @{command_spec "function"}
   294     "define general recursive functions"
   295     (function_parser default_config
   296       >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
   297 
   298 val _ =
   299   Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
   300     "prove termination of a recursive function"
   301     (Scan.option Parse.term >> termination_cmd)
   302 
   303 
   304 end