wenzelm@18620: (* Title: Pure/Isar/specification.ML wenzelm@18620: ID: $Id$ wenzelm@18620: Author: Makarius wenzelm@18620: wenzelm@21036: Derived local theory specifications --- with type-inference and wenzelm@18810: toplevel polymorphism. wenzelm@18620: *) wenzelm@18620: wenzelm@18620: signature SPECIFICATION = wenzelm@18620: sig wenzelm@20890: val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit wenzelm@24724: val check_specification: (string * typ option * mixfix) list -> wenzelm@24724: ((string * Attrib.src list) * term list) list list -> Proof.context -> wenzelm@18771: (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * wenzelm@24724: Proof.context wenzelm@24927: val read_specification: (string * string option * mixfix) list -> wenzelm@24927: ((string * Attrib.src list) * string list) list list -> Proof.context -> wenzelm@18771: (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * wenzelm@24724: Proof.context wenzelm@24724: val check_free_specification: (string * typ option * mixfix) list -> wenzelm@24724: ((string * Attrib.src list) * term list) list -> Proof.context -> wenzelm@24724: (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * wenzelm@24724: Proof.context wenzelm@24927: val read_free_specification: (string * string option * mixfix) list -> wenzelm@24927: ((string * Attrib.src list) * string list) list -> Proof.context -> wenzelm@24927: (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * wenzelm@24927: Proof.context wenzelm@24927: val axiomatization: (string * typ option * mixfix) list -> wenzelm@24927: ((bstring * Attrib.src list) * term list) list -> local_theory -> wenzelm@24927: (term list * (bstring * thm list) list) * local_theory wenzelm@24927: val axiomatization_cmd: (string * string option * mixfix) list -> wenzelm@18954: ((bstring * Attrib.src list) * string list) list -> local_theory -> wenzelm@18954: (term list * (bstring * thm list) list) * local_theory wenzelm@18954: val definition: wenzelm@21705: (string * typ option * mixfix) option * ((string * Attrib.src list) * term) -> wenzelm@21705: local_theory -> (term * (bstring * thm)) * local_theory wenzelm@24927: val definition_cmd: wenzelm@24927: (string * string option * mixfix) option * ((string * Attrib.src list) * string) -> wenzelm@24927: local_theory -> (term * (bstring * thm)) * local_theory wenzelm@24927: val abbreviation: Syntax.mode -> (string * typ option * mixfix) option * term -> wenzelm@21532: local_theory -> local_theory wenzelm@24927: val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string -> wenzelm@24927: local_theory -> local_theory wenzelm@24949: val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory wenzelm@24949: val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory wenzelm@24927: val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list wenzelm@20914: -> local_theory -> (bstring * thm list) list * local_theory wenzelm@24927: val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list wenzelm@20914: -> local_theory -> (bstring * thm list) list * local_theory wenzelm@24986: val theorem: string -> Method.text option -> wenzelm@24986: (thm list list -> local_theory -> local_theory) -> wenzelm@24927: string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i -> berghofe@24452: bool -> local_theory -> Proof.state wenzelm@24986: val theorem_cmd: string -> Method.text option -> wenzelm@24986: (thm list list -> local_theory -> local_theory) -> wenzelm@24927: string * Attrib.src list -> Element.context Locale.element list -> Element.statement -> berghofe@24452: bool -> local_theory -> Proof.state berghofe@24452: val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic wenzelm@18620: end; wenzelm@18620: wenzelm@18620: structure Specification: SPECIFICATION = wenzelm@18620: struct wenzelm@18620: wenzelm@21230: wenzelm@20890: (* diagnostics *) wenzelm@20890: wenzelm@20890: fun print_consts _ _ [] = () wenzelm@24986: | print_consts ctxt pred cs = Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs); wenzelm@20914: wenzelm@19664: wenzelm@18620: (* prepare specification *) wenzelm@18620: wenzelm@24724: local wenzelm@24724: wenzelm@24724: fun close_forms ctxt i xs As = wenzelm@24724: let wenzelm@24724: fun add_free (Free (x, _)) = if Variable.is_fixed ctxt x then I else insert (op =) x wenzelm@24724: | add_free _ = I; wenzelm@24724: wenzelm@24724: val commons = map #1 xs; wenzelm@24724: val _ = wenzelm@24724: (case duplicates (op =) commons of [] => () wenzelm@24724: | dups => error ("Duplicate local variables " ^ commas_quote dups)); wenzelm@24724: val frees = rev ((fold o fold_aterms) add_free As (rev commons)); wenzelm@24848: val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context Name.aT (length frees)); wenzelm@24724: val uniform_typing = the o AList.lookup (op =) (frees ~~ types); wenzelm@24724: wenzelm@24724: fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b) wenzelm@24724: | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u wenzelm@24724: | abs_body lev y (t as Free (x, T)) = wenzelm@24724: if x = y then TypeInfer.constrain (uniform_typing x) (TypeInfer.constrain T (Bound lev)) wenzelm@24724: else t wenzelm@24724: | abs_body _ _ a = a; wenzelm@24724: fun close (y, U) B = wenzelm@24724: let val B' = abs_body 0 y (Term.incr_boundvars 1 B) wenzelm@24724: in if Term.loose_bvar1 (B', 0) then Term.all dummyT $ Abs (y, U, B') else B end; wenzelm@24724: fun close_form A = wenzelm@24724: let wenzelm@24724: val occ_frees = rev (fold_aterms add_free A []); wenzelm@24724: val bounds = xs @ map (rpair dummyT) (subtract (op =) commons occ_frees); wenzelm@24724: in fold_rev close bounds A end; wenzelm@24724: in map close_form As end; wenzelm@24724: wenzelm@24724: fun prep_spec prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt = wenzelm@18620: let wenzelm@18670: val thy = ProofContext.theory_of ctxt; wenzelm@18620: wenzelm@18670: val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars; wenzelm@18670: val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; wenzelm@18620: wenzelm@24724: val Asss = (map o map) (map (parse_prop params_ctxt) o snd) raw_specss; wenzelm@24734: val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss) wenzelm@24734: |> fold Name.declare xs; wenzelm@24734: val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names); wenzelm@24734: val idx = (fold o fold o fold) Term.maxidx_term Asss' ~1 + 1; wenzelm@24724: val specs = wenzelm@24724: (if do_close then wenzelm@24734: #1 (fold_map wenzelm@24734: (fn Ass => fn i => (burrow (close_forms params_ctxt i []) Ass, i + 1)) Asss' idx) wenzelm@24734: else Asss') wenzelm@24724: |> flat |> burrow (Syntax.check_props params_ctxt); wenzelm@24724: val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs; wenzelm@24724: wenzelm@24724: val vs = specs_ctxt |> fold_map ProofContext.inferred_param xs |> fst; wenzelm@18771: val params = vs ~~ map #3 vars; wenzelm@24724: val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss); wenzelm@24724: in ((params, name_atts ~~ specs), specs_ctxt) end; wenzelm@24724: wenzelm@24724: fun read_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src x; wenzelm@24724: fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) x; wenzelm@18620: wenzelm@24724: in wenzelm@21370: wenzelm@24724: fun read_specification x = read_spec true x; wenzelm@24724: fun check_specification x = check_spec true x; wenzelm@24724: fun read_free_specification vars specs = read_spec false vars [specs]; wenzelm@24724: fun check_free_specification vars specs = check_spec false vars [specs]; wenzelm@24724: wenzelm@24724: end; wenzelm@18620: wenzelm@18620: wenzelm@18771: (* axiomatization *) wenzelm@18620: wenzelm@20890: fun gen_axioms prep raw_vars raw_specs lthy = wenzelm@18620: let wenzelm@24986: val ((vars, specs), _) = prep raw_vars [raw_specs] lthy; wenzelm@24986: val ((consts, axioms), lthy') = LocalTheory.axioms Thm.axiomK (vars, specs) lthy; wenzelm@24724: val consts' = map (Morphism.term (LocalTheory.target_morphism lthy')) consts; wenzelm@24986: val _ = print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) (map fst vars); wenzelm@24986: in ((consts, axioms), lthy') end; wenzelm@18786: wenzelm@24927: val axiomatization = gen_axioms check_specification; wenzelm@24927: val axiomatization_cmd = gen_axioms read_specification; wenzelm@18620: wenzelm@18786: wenzelm@18786: (* definition *) wenzelm@18786: wenzelm@21705: fun gen_def prep (raw_var, (raw_a, raw_prop)) lthy = wenzelm@18786: let wenzelm@21705: val (vars, [((raw_name, atts), [prop])]) = wenzelm@21705: fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy); wenzelm@21705: val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop; wenzelm@21705: val name = Thm.def_name_optional x raw_name; wenzelm@21705: val mx = (case vars of [] => NoSyn | [((x', _), mx)] => wenzelm@21705: if x = x' then mx wenzelm@21705: else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x')); wenzelm@21705: val ((lhs, (_, th)), lthy2) = lthy wenzelm@25016: |> LocalTheory.define Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs)); wenzelm@21705: val ((b, [th']), lthy3) = lthy2 haftmann@22744: |> LocalTheory.note Thm.definitionK haftmann@24624: ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]); wenzelm@18786: wenzelm@21705: val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs; wenzelm@21705: val _ = print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)]; wenzelm@21705: in ((lhs, (b, th')), lthy3) end; wenzelm@18786: wenzelm@24927: val definition = gen_def check_free_specification; wenzelm@24927: val definition_cmd = gen_def read_free_specification; wenzelm@18786: wenzelm@19080: wenzelm@19080: (* abbreviation *) wenzelm@19080: wenzelm@21705: fun gen_abbrev prep mode (raw_var, raw_prop) lthy = wenzelm@19080: let wenzelm@21705: val ((vars, [(_, [prop])]), _) = wenzelm@21705: prep (the_list raw_var) [(("", []), [raw_prop])] wenzelm@24676: (lthy |> ProofContext.set_mode ProofContext.mode_abbrev); wenzelm@21705: val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop)); wenzelm@21705: val mx = (case vars of [] => NoSyn | [((y, _), mx)] => wenzelm@21705: if x = y then mx wenzelm@21705: else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y)); wenzelm@21705: val lthy' = lthy wenzelm@24986: |> ProofContext.set_syntax_mode mode (* FIXME ?!? *) wenzelm@21793: |> LocalTheory.abbrev mode ((x, mx), rhs) |> snd wenzelm@21705: |> ProofContext.restore_syntax_mode lthy; wenzelm@24724: wenzelm@21705: val _ = print_consts lthy' (K false) [(x, T)] wenzelm@21532: in lthy' end; wenzelm@19080: wenzelm@24927: val abbreviation = gen_abbrev check_free_specification; wenzelm@24927: val abbreviation_cmd = gen_abbrev read_free_specification; wenzelm@19080: wenzelm@19664: wenzelm@21230: (* notation *) wenzelm@19664: wenzelm@24949: fun gen_notation prep_const add mode args lthy = wenzelm@25371: lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args); wenzelm@19664: wenzelm@24927: val notation = gen_notation (K I); wenzelm@24927: val notation_cmd = gen_notation ProofContext.read_const; wenzelm@19664: wenzelm@20914: wenzelm@21036: (* fact statements *) wenzelm@20914: wenzelm@20914: fun gen_theorems prep_thms prep_att kind raw_facts lthy = wenzelm@20914: let wenzelm@20914: val attrib = prep_att (ProofContext.theory_of lthy); wenzelm@20914: val facts = raw_facts |> map (fn ((name, atts), bs) => wenzelm@20914: ((name, map attrib atts), wenzelm@21435: bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts)))); wenzelm@21435: val (res, lthy') = lthy |> LocalTheory.notes kind facts; wenzelm@24986: val _ = ProofDisplay.present_results lthy' ((kind, ""), res); wenzelm@20914: in (res, lthy') end; wenzelm@20914: wenzelm@24927: val theorems = gen_theorems (K I) (K I); wenzelm@24927: val theorems_cmd = gen_theorems ProofContext.get_thms Attrib.intern_src; wenzelm@20914: wenzelm@21036: wenzelm@21230: (* complex goal statements *) wenzelm@21036: wenzelm@21036: local wenzelm@21036: wenzelm@21450: fun subtract_prems ctxt1 ctxt2 = wenzelm@21450: Library.drop (length (Assumption.prems_of ctxt1), Assumption.prems_of ctxt2); wenzelm@21450: wenzelm@21236: fun prep_statement prep_att prep_stmt elems concl ctxt = wenzelm@21236: (case concl of wenzelm@21236: Element.Shows shows => wenzelm@21230: let wenzelm@21450: val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt; wenzelm@21450: val prems = subtract_prems loc_ctxt elems_ctxt; wenzelm@21450: val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp); wenzelm@21370: val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt; wenzelm@21450: in ((prems, stmt, []), goal_ctxt) end wenzelm@21236: | Element.Obtains obtains => wenzelm@21230: let wenzelm@21236: val case_names = obtains |> map_index wenzelm@21236: (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name); wenzelm@21236: val constraints = obtains |> map (fn (_, (vars, _)) => wenzelm@21236: Locale.Elem (Element.Constrains wenzelm@21236: (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE)))); wenzelm@21036: wenzelm@21236: val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props); wenzelm@21450: val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt; wenzelm@21236: wenzelm@21236: val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN; wenzelm@21036: wenzelm@21236: fun assume_case ((name, (vars, _)), asms) ctxt' = wenzelm@21236: let wenzelm@21236: val xs = map fst vars; wenzelm@21236: val props = map fst asms; wenzelm@21236: val (parms, _) = ctxt' wenzelm@21236: |> fold Variable.declare_term props wenzelm@21236: |> fold_map ProofContext.inferred_param xs; wenzelm@21236: val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis)); wenzelm@21236: in wenzelm@21236: ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs)); wenzelm@21370: ctxt' |> Variable.auto_fixes asm wenzelm@21236: |> ProofContext.add_assms_i Assumption.assume_export wenzelm@21236: [((name, [ContextRules.intro_query NONE]), [(asm, [])])] wenzelm@21236: |>> (fn [(_, [th])] => th) wenzelm@21236: end; wenzelm@21236: wenzelm@21658: val atts = map (Attrib.internal o K) wenzelm@21236: [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names]; wenzelm@21450: val prems = subtract_prems loc_ctxt elems_ctxt; wenzelm@21236: val stmt = [(("", atts), [(thesis, [])])]; wenzelm@21236: wenzelm@21236: val (facts, goal_ctxt) = elems_ctxt wenzelm@21236: |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)]) wenzelm@21236: |> fold_map assume_case (obtains ~~ propp) wenzelm@21435: |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK wenzelm@21435: [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths); wenzelm@21450: in ((prems, stmt, facts), goal_ctxt) end); wenzelm@21036: berghofe@24452: structure TheoremHook = GenericDataFun berghofe@24452: ( berghofe@24452: type T = ((bool -> Proof.state -> Proof.state) * stamp) list; berghofe@24452: val empty = []; berghofe@24452: val extend = I; wenzelm@24464: fun merge _ hooks : T = Library.merge (eq_snd op =) hooks; berghofe@24452: ); berghofe@24452: wenzelm@21036: fun gen_theorem prep_att prep_stmt berghofe@24452: kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy0 = wenzelm@21036: let wenzelm@21860: val _ = LocalTheory.affirm lthy0; wenzelm@21036: val thy = ProofContext.theory_of lthy0; wenzelm@21206: wenzelm@21036: val (loc, ctxt, lthy) = wenzelm@21036: (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of wenzelm@25011: ({target, is_locale = true, ...}, true) => wenzelm@25011: (*temporary workaround for non-modularity of in/includes*) (* FIXME *) wenzelm@25011: (SOME target, ProofContext.init thy, LocalTheory.restore lthy0) wenzelm@21036: | _ => (NONE, lthy0, lthy0)); wenzelm@21036: wenzelm@21435: val attrib = prep_att thy; wenzelm@21435: val atts = map attrib raw_atts; wenzelm@21435: wenzelm@21532: val elems = raw_elems |> map (Locale.map_elem (Element.map_ctxt_attrib attrib)); wenzelm@21450: val ((prems, stmt, facts), goal_ctxt) = wenzelm@21450: prep_statement attrib (prep_stmt loc) elems raw_concl ctxt; wenzelm@21036: wenzelm@21036: fun after_qed' results goal_ctxt' = wenzelm@21602: let val results' = wenzelm@21602: burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results wenzelm@21602: in wenzelm@21036: lthy wenzelm@21435: |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results') wenzelm@21036: |> (fn (res, lthy') => wenzelm@24986: (ProofDisplay.present_results lthy' ((kind, name), res); wenzelm@21435: if name = "" andalso null atts then lthy' wenzelm@21435: else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy'))) wenzelm@21036: |> after_qed results' wenzelm@21036: end; wenzelm@21036: in wenzelm@21036: goal_ctxt wenzelm@21450: |> ProofContext.note_thmss_i Thm.assumptionK [((AutoBind.assmsN, []), [(prems, [])])] wenzelm@21450: |> snd wenzelm@21435: |> Proof.theorem_i before_qed after_qed' (map snd stmt) wenzelm@24557: |> Proof.refine_insert facts wenzelm@24542: |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt)))) wenzelm@21036: end; wenzelm@21036: wenzelm@21230: in wenzelm@21230: wenzelm@24927: val theorem = gen_theorem (K I) Locale.cert_context_statement; wenzelm@24927: val theorem_cmd = gen_theorem Attrib.intern_src Locale.read_context_statement_i; wenzelm@21036: berghofe@24452: fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ())); berghofe@24452: wenzelm@18620: end; wenzelm@21036: wenzelm@21036: end;