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