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