# HG changeset patch # User paulson # Date 1568910255 -3600 # Node ID da7c0df11a04fc3a14c4953045838249670fafef # Parent dea35c31a0b852f73e157f0f428c45325195b1dc# Parent e4825ec2046893c15240bedf6eb1292de0cdcb59 merged diff -r e4825ec20468 -r da7c0df11a04 src/HOL/Eisbach/Tests.thy --- a/src/HOL/Eisbach/Tests.thy Thu Sep 19 17:24:08 2019 +0100 +++ b/src/HOL/Eisbach/Tests.thy Thu Sep 19 17:24:15 2019 +0100 @@ -166,7 +166,7 @@ done (* Cut tests *) - fix A B C + fix A B C D have "D \ C \ A \ B \ A \ C \ D \ True \ C" by (((match premises in I: "P \ Q" (cut) diff -r e4825ec20468 -r da7c0df11a04 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Thu Sep 19 17:24:08 2019 +0100 +++ b/src/Pure/Isar/obtain.ML Thu Sep 19 17:24:15 2019 +0100 @@ -201,7 +201,7 @@ val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state); - val ((vars, propss, binds, binds'), params_ctxt) = + val ({vars, propss, binds, result_binds, ...}, params_ctxt) = prep_stmt (raw_decls @ raw_fixes) (raw_prems @ map #2 raw_concls) thesis_ctxt; val (decls, fixes) = chop (length raw_decls) vars ||> map #2; val (premss, conclss) = chop (length raw_prems) propss; @@ -230,7 +230,7 @@ [((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])] [(Binding.empty_atts, [(thesis, [])])] int |-> Proof.refine_insert - |> Proof.map_context (fold Variable.bind_term binds') + |> Proof.map_context (fold Variable.bind_term result_binds) end; in diff -r e4825ec20468 -r da7c0df11a04 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Sep 19 17:24:08 2019 +0100 +++ b/src/Pure/Isar/proof.ML Thu Sep 19 17:24:15 2019 +0100 @@ -557,16 +557,36 @@ local -fun gen_bind bind args state = - state - |> assert_forward - |> map_context (bind true args #> snd) - |> reset_facts; +fun gen_bind prep_terms raw_binds = + assert_forward #> map_context (fn ctxt => + let + fun prep_bind (raw_pats, t) ctxt1 = + let + val T = Term.fastype_of t; + val ctxt2 = Variable.declare_term t ctxt1; + val pats = prep_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt2) T raw_pats; + val binds = Proof_Context.simult_matches ctxt2 (t, pats); + in (binds, ctxt2) end; + + val ts = prep_terms ctxt dummyT (map snd raw_binds); + val (binds, ctxt') = apfst flat (fold_map prep_bind (map fst raw_binds ~~ ts) ctxt); + val binds' = map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds); + + val ctxt'' = + ctxt + |> fold Variable.declare_term (map #2 binds') + |> fold Proof_Context.bind_term binds'; + val _ = Variable.warn_extra_tfrees ctxt ctxt''; + in ctxt'' end) + #> reset_facts; + +fun read_terms ctxt T = + map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt; in -val let_bind = gen_bind Proof_Context.match_bind; -val let_bind_cmd = gen_bind Proof_Context.match_bind_cmd; +val let_bind = gen_bind (fn ctxt => fn _ => map (Proof_Context.cert_term ctxt)); +val let_bind_cmd = gen_bind read_terms; end; @@ -625,15 +645,15 @@ 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), _) = - prep_statement raw_fixes raw_prems (map snd raw_concls) ctxt; + val {fixes = params, assumes = prems_propss, shows = concl_propss, result_binds, text, ...} = + #1 (prep_statement 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 |> map_context_result (fn ctxt => ctxt - |> (fold o fold) Variable.declare_term propss + |> Proof_Context.augment text |> fold Variable.maybe_bind_term result_binds |> fold_burrow (Assumption.add_assms export o map (Thm.cterm_of ctxt)) propss |-> (fn premss => @@ -792,7 +812,7 @@ val ctxt = context_of state; (*vars*) - val ((vars, propss, _, binds'), vars_ctxt) = + val ({vars, propss, result_binds, ...}, vars_ctxt) = prep_stmt (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; @@ -826,7 +846,7 @@ raw_defs def_thmss; in state - |> map_context (K defs_ctxt #> fold Variable.bind_term binds') + |> map_context (K defs_ctxt #> fold Variable.bind_term result_binds) |> note_thmss notes end; @@ -1037,13 +1057,15 @@ (if strict_asm then Assumption.assume_export else Assumption.presume_export); (*params*) - val ((params, assumes_propss, shows_propss, result_binds), params_ctxt) = ctxt + val ({fixes = params, assumes = assumes_propss, shows = shows_propss, + result_binds, result_text, text}, params_ctxt) = ctxt |> prep_statement raw_fixes (map snd raw_assumes) (map snd raw_shows); (*prems*) val (assumes_bindings, shows_bindings) = apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows); val (that_fact, goal_ctxt) = params_ctxt + |> fold Proof_Context.augment (text :: flat (assumes_propss @ shows_propss)) |> fold_burrow add_assumes ((map o map) (Thm.cterm_of params_ctxt) assumes_propss) |> (fn (premss, ctxt') => let @@ -1063,12 +1085,13 @@ let val ctxt' = context_of state'; val export0 = - Assumption.export false result_ctxt ctxt' #> + Assumption.export false result_ctxt (Proof_Context.augment result_text ctxt') #> fold_rev (fn (x, v) => Thm.forall_intr_name (x, Thm.cterm_of params_ctxt v)) params #> Raw_Simplifier.norm_hhf_protect ctxt'; val export = map export0 #> Variable.export result_ctxt ctxt'; in state' + |> map_context (Proof_Context.augment result_text) |> local_results (results_bindings ~~ burrow export results) |-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit)) |> after_qed (result_ctxt, results) diff -r e4825ec20468 -r da7c0df11a04 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Sep 19 17:24:08 2019 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Sep 19 17:24:15 2019 +0100 @@ -108,10 +108,9 @@ val norm_export_morphism: Proof.context -> Proof.context -> morphism val auto_bind_goal: term list -> Proof.context -> Proof.context val auto_bind_facts: term list -> Proof.context -> Proof.context - val match_bind: bool -> (term list * term) list -> Proof.context -> - term list * Proof.context - val match_bind_cmd: bool -> (string list * string) list -> Proof.context -> - term list * Proof.context + val simult_matches: Proof.context -> term * term list -> (indexname * term) list + val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context + val bind_term: indexname * term -> Proof.context -> Proof.context val cert_propp: Proof.context -> (term * term list) list list -> (term list list * (indexname * term) list) val read_propp: Proof.context -> (string * string list) list list -> @@ -170,22 +169,28 @@ 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_stmt: - (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_stmt: - (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 + type stmt = + {vars: ((binding * typ option * mixfix) * (string * term)) list, + propss: term list list, + binds: (indexname * term) list, + result_binds: (indexname * term) list} + val cert_stmt: (binding * typ option * mixfix) list -> (term * term list) list list -> + Proof.context -> stmt * Proof.context + val read_stmt: (binding * string option * mixfix) list -> (string * string list) list list -> + Proof.context -> stmt * Proof.context + type statement = + {fixes: (string * term) list, + assumes: term list list, + shows: term list list, + result_binds: (indexname * term option) list, + text: term, + result_text: term} val cert_statement: (binding * typ option * mixfix) list -> (term * term list) list list -> (term * term list) list list -> Proof.context -> - ((string * term) list * term list list * term list list * (indexname * term option) list) * - Proof.context + statement * Proof.context val read_statement: (binding * string option * mixfix) list -> (string * string list) list list -> (string * string list) list list -> Proof.context -> - ((string * term) list * term list list * term list list * (indexname * term option) list) * - Proof.context + statement * Proof.context val print_syntax: Proof.context -> unit val print_abbrevs: bool -> Proof.context -> unit val pretty_term_bindings: Proof.context -> Pretty.T list @@ -418,8 +423,7 @@ (* augment context by implicit term declarations *) fun augment t ctxt = ctxt - |> not (Variable.is_body ctxt) ? - Variable.add_fixes_direct (rev (Variable.add_free_names ctxt t [])) + |> Variable.add_fixes_implicit t |> Variable.declare_term t |> Soft_Type_System.augment t; @@ -849,15 +853,7 @@ (** term bindings **) -(* simult_matches *) - -fun simult_matches ctxt (t, pats) = - (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of - NONE => error "Pattern match failed!" - | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []); - - -(* auto_bind *) +(* auto bindings *) fun auto_bind f props ctxt = fold Variable.maybe_bind_term (f ctxt props) ctxt; @@ -865,52 +861,18 @@ val auto_bind_facts = auto_bind Auto_Bind.facts; -(* bind terms (non-schematic) *) +(* match bindings *) -fun cert_maybe_bind_term (xi, t) ctxt = +fun simult_matches ctxt (t, pats) = + (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of + NONE => error "Pattern match failed!" + | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []); + +fun maybe_bind_term (xi, t) ctxt = ctxt |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t); -val cert_bind_term = cert_maybe_bind_term o apsnd SOME; - - -(* match_bind *) - -local - -fun gen_bind prep_terms gen raw_binds ctxt = - let - fun prep_bind (raw_pats, t) ctxt1 = - let - val T = Term.fastype_of t; - val ctxt2 = Variable.declare_term t ctxt1; - val pats = prep_terms (set_mode mode_pattern ctxt2) T raw_pats; - val binds = simult_matches ctxt2 (t, pats); - in (binds, ctxt2) end; - - val ts = prep_terms ctxt dummyT (map snd raw_binds); - val (binds, ctxt') = apfst flat (fold_map prep_bind (map fst raw_binds ~~ ts) ctxt); - val binds' = - if gen then map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds) - else binds; - val ctxt'' = - tap (Variable.warn_extra_tfrees ctxt) - (if gen then - ctxt (*sic!*) - |> fold Variable.declare_term (map #2 binds') - |> fold cert_bind_term binds' - else ctxt' |> fold cert_bind_term binds'); - in (ts, ctxt'') end; - -in - -fun read_terms ctxt T = - map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt; - -val match_bind = gen_bind (fn ctxt => fn _ => map (cert_term ctxt)); -val match_bind_cmd = gen_bind read_terms; - -end; +val bind_term = maybe_bind_term o apsnd SOME; (* propositions with patterns *) @@ -1347,7 +1309,7 @@ val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c; in ctxt' - |> fold (cert_maybe_bind_term o drop_schematic) binds + |> fold (maybe_bind_term o drop_schematic) binds |> update_cases (map (apsnd SOME) cases) |> pair (assumes, (binds, cases)) end; @@ -1378,6 +1340,20 @@ (* structured statements *) +type stmt = + {vars: ((binding * typ option * mixfix) * (string * term)) list, + propss: term list list, + binds: (indexname * term) list, + result_binds: (indexname * term) list}; + +type statement = + {fixes: (string * term) list, + assumes: term list list, + shows: term list list, + result_binds: (indexname * term option) list, + text: term, + result_text: term}; + local fun export_binds ctxt' ctxt params binds = @@ -1407,13 +1383,15 @@ |> map (apsnd the); val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt; - in ((vars' ~~ params, propss, binds, binds'), params_ctxt) end; + val result : stmt = + {vars = vars' ~~ params, propss = propss, binds = binds, result_binds = binds'}; + in (result, params_ctxt) end; fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt = let val ((fixes, (assumes, shows), binds), ctxt') = ctxt |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows) - |-> (fn (vars, propss, binds, _) => + |-> (fn {vars, propss, binds, ...} => fold Variable.bind_term binds #> pair (map #2 vars, chop (length raw_assumes) propss, binds)); val binds' = @@ -1422,7 +1400,18 @@ NONE => [] | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds)) |> export_binds ctxt' ctxt fixes; - in ((fixes, assumes, shows, binds'), ctxt') end; + + val text = Logic.close_prop fixes (flat assumes) (Logic.mk_conjunction_list (flat shows)); + val text' = singleton (Variable.export_terms ctxt' ctxt) text; + + val result : statement = + {fixes = fixes, + assumes = assumes, + shows = shows, + result_binds = binds', + text = text, + result_text = text'}; + in (result, ctxt') end; in diff -r e4825ec20468 -r da7c0df11a04 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Thu Sep 19 17:24:08 2019 +0100 +++ b/src/Pure/Isar/specification.ML Thu Sep 19 17:24:15 2019 +0100 @@ -204,7 +204,7 @@ fun gen_axioms prep_stmt prep_att raw_decls raw_fixes raw_prems raw_concls thy = let (*specification*) - val ((vars, [prems, concls], _, _), vars_ctxt) = + val ({vars, propss = [prems, concls], ...}, vars_ctxt) = Proof_Context.init_global thy |> prep_stmt (raw_decls @ raw_fixes) ((map o map) (rpair []) [raw_prems, map snd raw_concls]); val (decls, fixes) = chop (length raw_decls) vars; diff -r e4825ec20468 -r da7c0df11a04 src/Pure/assumption.ML --- a/src/Pure/assumption.ML Thu Sep 19 17:24:08 2019 +0100 +++ b/src/Pure/assumption.ML Thu Sep 19 17:24:15 2019 +0100 @@ -85,13 +85,33 @@ (* local assumptions *) +local + +fun drop_prefix eq (args as (x :: xs, y :: ys)) = + if eq (x, y) then drop_prefix eq (xs, ys) else args + | drop_prefix _ args = args; + +fun check_result ctxt kind term_of res = + (case res of + ([], rest) => rest + | (bad :: _, _) => + raise Fail ("Outer context disagrees on " ^ kind ^ ": " ^ + Syntax.string_of_term ctxt (term_of bad))); + +in + fun local_assumptions_of inner outer = - drop (length (all_assumptions_of outer)) (all_assumptions_of inner); + drop_prefix (eq_snd (eq_list Thm.aconvc)) (apply2 all_assumptions_of (outer, inner)) + |>> maps #2 + |> check_result outer "assumption" Thm.term_of; val local_assms_of = maps #2 oo local_assumptions_of; fun local_prems_of inner outer = - drop (length (all_prems_of outer)) (all_prems_of inner); + drop_prefix Thm.eq_thm_prop (apply2 all_prems_of (outer, inner)) + |> check_result outer "premise" Thm.prop_of; + +end; (* add assumptions *) diff -r e4825ec20468 -r da7c0df11a04 src/Pure/variable.ML --- a/src/Pure/variable.ML Thu Sep 19 17:24:08 2019 +0100 +++ b/src/Pure/variable.ML Thu Sep 19 17:24:15 2019 +0100 @@ -58,6 +58,7 @@ val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context val add_fixes: string list -> Proof.context -> string list * Proof.context val add_fixes_direct: string list -> Proof.context -> Proof.context + val add_fixes_implicit: term -> Proof.context -> Proof.context val fix_dummy_patterns: term -> Proof.context -> term * Proof.context val variant_fixes: string list -> Proof.context -> string list * Proof.context val gen_all: Proof.context -> thm -> thm @@ -475,6 +476,9 @@ |> (snd o add_fixes xs) |> restore_body ctxt; +fun add_fixes_implicit t ctxt = ctxt + |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t [])); + (* dummy patterns *)