# HG changeset patch # User wenzelm # Date 1461680428 -7200 # Node ID 9b95ae9ec6719d98b9cf7c36e843b362ebc56ee3 # Parent ae0ca486bd3fe3d737d8e77a741d84b9071c9401 defs are closed, which leads to proper auto_bind_facts; misc tuning; diff -r ae0ca486bd3f -r 9b95ae9ec671 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Tue Apr 26 11:56:06 2016 +0200 +++ b/src/Pure/Isar/obtain.ML Tue Apr 26 16:20:28 2016 +0200 @@ -193,27 +193,27 @@ local -fun gen_obtain prep_spec prep_att that_binding raw_vars raw_asms int state = +fun gen_obtain prep_statement prep_att that_binding raw_vars raw_asms int state = let val _ = Proof.assert_forward_or_chain state; val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state); + val ((vars, propss, binds, binds'), params_ctxt) = + prep_statement raw_vars (map #2 raw_asms) thesis_ctxt; + val params = map #2 vars; + val that_prop = + Logic.list_rename_params (map #1 params) + (fold_rev Logic.all (map #2 params) (Logic.list_implies (flat propss, thesis))); - val (((vars, xs, params), propss, binds, binds'), params_ctxt) = - prep_spec raw_vars (map #2 raw_asms) thesis_ctxt; - val cparams = map (Thm.cterm_of params_ctxt) params; + val cparams = map (Thm.cterm_of params_ctxt o #2 o #2) vars; val asms = map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_asms ~~ map (map (rpair [])) propss; - val that_prop = - Logic.list_rename_params xs - (fold_rev Logic.all params (Logic.list_implies (flat propss, thesis))); - fun after_qed (result_ctxt, results) state' = let val [rule] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) in state' - |> Proof.fix vars + |> Proof.fix (map #1 vars) |> Proof.map_context (fold Variable.bind_term binds) |> Proof.assm (obtain_export params_ctxt rule cparams) [] [] asms end; @@ -229,8 +229,8 @@ in -val obtain = gen_obtain Proof_Context.cert_spec (K I); -val obtain_cmd = gen_obtain Proof_Context.read_spec Attrib.attribute_cmd; +val obtain = gen_obtain Proof_Context.cert_statement (K I); +val obtain_cmd = gen_obtain Proof_Context.read_statement Attrib.attribute_cmd; end; diff -r ae0ca486bd3f -r 9b95ae9ec671 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Apr 26 11:56:06 2016 +0200 +++ b/src/Pure/Isar/proof.ML Tue Apr 26 16:20:28 2016 +0200 @@ -694,13 +694,9 @@ val ctxt = context_of state; val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls; - val (params, prems_propss, concl_propss, result_binds) = - #1 (prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt); - - fun close prop = - fold_rev Logic.dependent_all_name params - (Logic.list_implies (flat prems_propss, prop)); - val propss = (map o map) close concl_propss; + val ((params, prems_propss, concl_propss, result_binds), _) = + prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt; + val propss = (map o map) (Logic.close_prop params (flat prems_propss)) concl_propss; in state |> assert_forward @@ -893,45 +889,37 @@ local -fun match_defs (((b, _, mx), x) :: more_decls) ((((a, _), t), _) :: more_defs) = - if x = a then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs - else error ("Mismatch of declaration " ^ quote x ^ " wrt. definition " ^ quote a) - | match_defs [] [] = [] - | match_defs more_decls more_defs = - error ("Mismatch of declarations " ^ commas_quote (map #2 more_decls) ^ - (if null more_decls then "" else " ") ^ - "wrt. definitions " ^ commas_quote (map (#1 o #1 o #1) more_defs)); - -fun invisible_fixes vars ctxt = ctxt - |> Context_Position.set_visible false - |> Proof_Context.add_fixes vars |> #2 - |> Context_Position.restore_visible ctxt; - -fun gen_define prep_spec prep_att raw_vars raw_fixes raw_defs state = +fun gen_define prep_statement prep_att raw_decls raw_fixes raw_defs state = let val _ = assert_forward state; val ctxt = context_of state; (*vars*) - val n_vars = length raw_vars; - val (((all_vars, _, all_params), defss, _, binds'), _) = - prep_spec (raw_vars @ raw_fixes) (map snd raw_defs) ctxt; - val (vars, fixes) = chop n_vars all_vars; - val (params, _) = chop n_vars all_params; + val ((vars, propss, _, binds'), vars_ctxt) = + prep_statement (raw_decls @ raw_fixes) (map snd raw_defs) ctxt; + val (decls, fixes) = chop (length raw_decls) vars; + val show_term = Syntax.string_of_term vars_ctxt; (*defs*) - val derived_def = Local_Defs.derived_def (invisible_fixes vars ctxt) {conditional = false}; - val defs1 = map derived_def (flat defss); - val defs2 = match_defs (vars ~~ map (#1 o dest_Free) params) defs1; + fun match_defs (((b, _, mx), (_, Free (x, T))) :: more_decls) ((((y, U), t), _) :: more_defs) = + if x = y then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs + else + error ("Mismatch of declaration " ^ show_term (Free (x, T)) ^ " wrt. definition " ^ + show_term (Free (y, U))) + | match_defs [] [] = [] + | match_defs more_decls more_defs = + error ("Mismatch of declarations " ^ commas (map (show_term o #2 o #2) more_decls) ^ + (if null more_decls then "" else " ") ^ + "wrt. definitions " ^ commas (map (show_term o Free o #1 o #1) more_defs)); + + val derived_def = Local_Defs.derived_def ctxt {conditional = false}; + val defs1 = map (derived_def o Logic.close_prop (map #2 fixes) []) (flat propss); + val defs2 = match_defs decls defs1; val (defs3, defs_ctxt) = Local_Defs.add_defs defs2 ctxt; - (*fixes*) - val fixes_ctxt = invisible_fixes fixes defs_ctxt; - val export = singleton (Variable.export fixes_ctxt defs_ctxt); - (*notes*) val def_thmss = - map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, export (prove fixes_ctxt th))) + map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, prove defs_ctxt th)) (defs1 ~~ defs2 ~~ defs3) |> unflat (map snd raw_defs); val notes = @@ -947,8 +935,8 @@ in -val define = gen_define Proof_Context.cert_spec (K I); -val define_cmd = gen_define Proof_Context.read_spec Attrib.attribute_cmd; +val define = gen_define Proof_Context.cert_statement (K I); +val define_cmd = gen_define Proof_Context.read_statement Attrib.attribute_cmd; end; diff -r ae0ca486bd3f -r 9b95ae9ec671 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Apr 26 11:56:06 2016 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Apr 26 16:20:28 2016 +0200 @@ -166,12 +166,14 @@ val generic_add_abbrev: string -> binding * term -> Context.generic -> (term * term) * Context.generic val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic - val cert_spec: (binding * typ option * mixfix) list -> (term * term list) list list -> - Proof.context -> (((binding * typ option * mixfix) list * string list * term list) * - term list list * (indexname * term) list * (indexname * term) list) * Proof.context - val read_spec: (binding * string option * mixfix) list -> (string * string list) list list -> - Proof.context -> (((binding * typ option * mixfix) list * string list * term list) * - term list list * (indexname * term) list * (indexname * term) list) * Proof.context + val cert_statement: + (binding * typ option * mixfix) list -> (term * term list) list list -> Proof.context -> + (((binding * typ option * mixfix) * (string * term)) list * term list list * + (indexname * term) list * (indexname * term) list) * Proof.context + val read_statement: + (binding * string option * mixfix) list -> (string * string list) list list -> Proof.context -> + (((binding * typ option * mixfix) * (string * term)) list * term list list * + (indexname * term) list * (indexname * term) list) * Proof.context val print_syntax: Proof.context -> unit val print_abbrevs: bool -> Proof.context -> unit val pretty_term_bindings: Proof.context -> Pretty.T list @@ -1326,38 +1328,32 @@ end; -(* specification with parameters *) +(* structured statement *) local -fun prep_spec prep_var prep_propp raw_vars raw_propps ctxt = +fun prep_statement prep_var prep_propp raw_vars raw_propps ctxt = let - (*vars*) - val ((xs', vars), vars_ctxt) = ctxt - |> fold_map prep_var raw_vars - |-> (fn vars => add_fixes vars ##>> pair vars); + val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt; val xs = map (Variable.check_name o #1) vars; - - (*propps*) - val (propss, binds) = prep_propp vars_ctxt raw_propps; - val props = flat propss; + val (xs', fixes_ctxt) = add_fixes vars vars_ctxt; - (*params*) - val (ps, params_ctxt) = vars_ctxt - |> fold Variable.declare_term props - |> fold Variable.bind_term binds + val (propss, binds) = prep_propp fixes_ctxt raw_propps; + val (ps, params_ctxt) = fixes_ctxt + |> (fold o fold) Variable.declare_term propss |> fold_map inferred_param xs'; - val params = map Free ps; - val binds' = (map o apsnd) (fold_rev Term.dependent_lambda_name (xs ~~ params)) binds; + val params = xs ~~ map Free ps; + val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps; + val binds' = (map o apsnd) (Logic.close_term params) binds; - val _ = Variable.warn_extra_tfrees vars_ctxt params_ctxt; - in (((vars', xs, params), propss, binds, binds'), params_ctxt) end; + val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt; + in ((vars' ~~ params, propss, binds, binds'), params_ctxt) end; in -val cert_spec = prep_spec cert_var cert_propp; -val read_spec = prep_spec read_var read_propp; +val cert_statement = prep_statement cert_var cert_propp; +val read_statement = prep_statement read_var read_propp; end; diff -r ae0ca486bd3f -r 9b95ae9ec671 src/Pure/logic.ML --- a/src/Pure/logic.ML Tue Apr 26 11:56:06 2016 +0200 +++ b/src/Pure/logic.ML Tue Apr 26 16:20:28 2016 +0200 @@ -26,6 +26,8 @@ val strip_prems: int * term list * term -> term list * term val count_prems: term -> int val nth_prem: int * term -> term + val close_term: (string * term) list -> term -> term + val close_prop: (string * term) list -> term list -> term -> term val true_prop: term val conjunction: term val mk_conjunction: term * term -> term @@ -147,7 +149,6 @@ end; - (** equality **) fun mk_equals (t, u) = @@ -204,6 +205,11 @@ fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); +(* close *) + +val close_term = fold_rev Term.dependent_lambda_name; +fun close_prop xs As B = fold_rev dependent_all_name xs (list_implies (As, B)); + (** conjunction **)