merged
authorwenzelm
Thu, 19 Sep 2019 16:38:32 +0200
changeset 70926 dea35c31a0b8
parent 70916 91587befabfd (current diff)
parent 70925 561b11865cb5 (diff)
child 70928 da7c0df11a04
child 70929 29243d779b61
merged
--- a/src/HOL/Eisbach/Tests.thy	Thu Sep 19 14:49:19 2019 +0100
+++ b/src/HOL/Eisbach/Tests.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -166,7 +166,7 @@
     done
 
   (* Cut tests *)
-  fix A B C
+  fix A B C D
 
   have "D \<and> C  \<Longrightarrow> A \<and> B  \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
     by (((match premises in I: "P \<and> Q" (cut)
--- a/src/Pure/Isar/obtain.ML	Thu Sep 19 14:49:19 2019 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Sep 19 16:38:32 2019 +0200
@@ -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
--- a/src/Pure/Isar/proof.ML	Thu Sep 19 14:49:19 2019 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Sep 19 16:38:32 2019 +0200
@@ -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)
--- a/src/Pure/Isar/proof_context.ML	Thu Sep 19 14:49:19 2019 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Sep 19 16:38:32 2019 +0200
@@ -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
 
--- a/src/Pure/Isar/specification.ML	Thu Sep 19 14:49:19 2019 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Sep 19 16:38:32 2019 +0200
@@ -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;
--- a/src/Pure/assumption.ML	Thu Sep 19 14:49:19 2019 +0100
+++ b/src/Pure/assumption.ML	Thu Sep 19 16:38:32 2019 +0200
@@ -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 *)
--- a/src/Pure/variable.ML	Thu Sep 19 14:49:19 2019 +0100
+++ b/src/Pure/variable.ML	Thu Sep 19 16:38:32 2019 +0200
@@ -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 *)