more uniform treatment of auto bindings vs. explicit user bindings;
authorwenzelm
Tue Jun 09 22:24:33 2015 +0200 (2015-06-09)
changeset 604081fd46ced2fa8
parent 60407 53ef7b78e78a
child 60409 240ad53041c9
more uniform treatment of auto bindings vs. explicit user bindings;
misc tuning;
NEWS
src/Pure/Isar/auto_bind.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/NEWS	Tue Jun 09 16:42:17 2015 +0200
     1.2 +++ b/NEWS	Tue Jun 09 22:24:33 2015 +0200
     1.3 @@ -12,6 +12,9 @@
     1.4  * Command 'obtain' binds term abbreviations (via 'is' patterns) in the
     1.5  proof body as well, abstracted over relevant parameters.
     1.6  
     1.7 +* Term abbreviations via 'is' patterns also work for schematic
     1.8 +statements: result is abstracted over unknowns.
     1.9 +
    1.10  * Local goal statements (commands 'have', 'show', 'hence', 'thus') allow
    1.11  an optional context of local variables ('for' declaration).
    1.12  
     2.1 --- a/src/Pure/Isar/auto_bind.ML	Tue Jun 09 16:42:17 2015 +0200
     2.2 +++ b/src/Pure/Isar/auto_bind.ML	Tue Jun 09 22:24:33 2015 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4    val thesisN: string
     2.5    val thisN: string
     2.6    val assmsN: string
     2.7 +  val abs_params: term -> term -> term
     2.8    val goal: Proof.context -> term list -> (indexname * term option) list
     2.9    val facts: Proof.context -> term list -> (indexname * term option) list
    2.10    val no_facts: indexname list
    2.11 @@ -25,8 +26,10 @@
    2.12  
    2.13  fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;
    2.14  
    2.15 +fun abs_params prop = fold_rev Term.abs (Logic.strip_params prop);
    2.16 +
    2.17  fun statement_binds ctxt name prop =
    2.18 -  [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment ctxt prop)))];
    2.19 +  [((name, 0), SOME (abs_params prop (strip_judgment ctxt prop)))];
    2.20  
    2.21  
    2.22  (* goal *)
    2.23 @@ -39,13 +42,14 @@
    2.24  
    2.25  fun get_arg ctxt prop =
    2.26    (case strip_judgment ctxt prop of
    2.27 -    _ $ t => SOME (fold_rev Term.abs (Logic.strip_params prop) t)
    2.28 +    _ $ t => SOME (abs_params prop t)
    2.29    | _ => NONE);
    2.30  
    2.31 -fun facts _ [] = []
    2.32 -  | facts ctxt props =
    2.33 -      let val prop = List.last props
    2.34 -      in [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop end;
    2.35 +fun facts ctxt props =
    2.36 +  (case try List.last props of
    2.37 +    NONE => []
    2.38 +  | SOME prop =>
    2.39 +      [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop);
    2.40  
    2.41  val no_facts = [Syntax_Ext.dddot_indexname, (thisN, 0)];
    2.42  
     3.1 --- a/src/Pure/Isar/obtain.ML	Tue Jun 09 16:42:17 2015 +0200
     3.2 +++ b/src/Pure/Isar/obtain.ML	Tue Jun 09 22:24:33 2015 +0200
     3.3 @@ -119,18 +119,20 @@
     3.4      val xs = map (Variable.check_name o #1) vars;
     3.5  
     3.6      (*obtain asms*)
     3.7 -    val (asm_propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
     3.8 -    val asm_props = flat asm_propss;
     3.9 -    val declare_asms = fold Variable.declare_term asm_props #> Proof_Context.bind_terms binds;
    3.10 +    val (propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
    3.11 +    val props = flat propss;
    3.12 +    val declare_asms =
    3.13 +      fold Variable.declare_term props #>
    3.14 +      fold Variable.bind_term binds;
    3.15      val asms =
    3.16        map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~
    3.17 -      map (map (rpair [])) asm_propss;
    3.18 +      map (map (rpair [])) propss;
    3.19  
    3.20      (*obtain params*)
    3.21      val (params, params_ctxt) =
    3.22        declare_asms fix_ctxt |> fold_map Proof_Context.inferred_param xs' |>> map Free;
    3.23      val cparams = map (Thm.cterm_of params_ctxt) params;
    3.24 -    val binds' = map (apsnd (fold_rev Term.dependent_lambda_name (xs ~~ params))) binds;
    3.25 +    val binds' = (map o apsnd) (fold_rev Term.dependent_lambda_name (xs ~~ params)) binds;
    3.26  
    3.27      val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
    3.28  
    3.29 @@ -141,7 +143,7 @@
    3.30      val that_name = if name = "" then thatN else name;
    3.31      val that_prop =
    3.32        Logic.list_rename_params xs
    3.33 -        (fold_rev Logic.all params (Logic.list_implies (asm_props, thesis)));
    3.34 +        (fold_rev Logic.all params (Logic.list_implies (props, thesis)));
    3.35      val obtain_prop =
    3.36        Logic.list_rename_params [Auto_Bind.thesisN]
    3.37          (Logic.all (Free thesis_var) (Logic.mk_implies (that_prop, thesis)));
     4.1 --- a/src/Pure/Isar/proof.ML	Tue Jun 09 16:42:17 2015 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Tue Jun 09 22:24:33 2015 +0200
     4.3 @@ -891,10 +891,6 @@
     4.4  
     4.5  local
     4.6  
     4.7 -fun export_binds ctxt' ctxt params binds =
     4.8 -  let val ts = map (fold_rev Term.dependent_lambda_name params o snd) binds;
     4.9 -  in map fst binds ~~ Variable.export_terms ctxt' ctxt ts end;
    4.10 -
    4.11  val is_var =
    4.12    can (dest_TVar o Logic.dest_type o Logic.dest_term) orf
    4.13    can (dest_Var o Logic.dest_term);
    4.14 @@ -916,11 +912,10 @@
    4.15  
    4.16  fun generic_goal kind before_qed after_qed make_statement state =
    4.17    let
    4.18 -    val ctxt = context_of state;
    4.19      val chaining = can assert_chain state;
    4.20      val pos = Position.thread_data ();
    4.21  
    4.22 -    val ((propss, params, binds), goal_state) =
    4.23 +    val ((propss, result_binds), goal_state) =
    4.24        state
    4.25        |> assert_forward_or_chain
    4.26        |> enter_forward
    4.27 @@ -928,7 +923,6 @@
    4.28        |> map_context_result make_statement;
    4.29      val props = flat propss;
    4.30      val goal_ctxt = context_of goal_state;
    4.31 -    val result_binds = export_binds goal_ctxt ctxt params binds;
    4.32  
    4.33      val vars = implicit_vars props;
    4.34      val propss' = vars :: propss;
    4.35 @@ -940,7 +934,7 @@
    4.36      val statement = ((kind, pos), propss', Thm.term_of goal);
    4.37  
    4.38      val after_qed' = after_qed |>> (fn after_local => fn results =>
    4.39 -      map_context (fold Variable.bind_term result_binds) #> after_local results);
    4.40 +      map_context (fold Variable.maybe_bind_term result_binds) #> after_local results);
    4.41    in
    4.42      goal_state
    4.43      |> map_context (init_context #> Variable.set_body true)
    4.44 @@ -955,22 +949,16 @@
    4.45      |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
    4.46    end;
    4.47  
    4.48 -fun generic_qed after_ctxt state =
    4.49 -  let
    4.50 -    val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state;
    4.51 -    val outer_state = state |> close_block;
    4.52 -    val outer_ctxt = context_of outer_state;
    4.53 -
    4.54 -    val props =
    4.55 -      flat (tl stmt)
    4.56 -      |> Variable.exportT_terms goal_ctxt outer_ctxt;
    4.57 -    val results =
    4.58 -      tl (conclude_goal goal_ctxt goal stmt)
    4.59 -      |> burrow (Proof_Context.export goal_ctxt outer_ctxt);
    4.60 -  in
    4.61 -    outer_state
    4.62 -    |> map_context (after_ctxt props)
    4.63 -    |> pair (after_qed, results)
    4.64 +fun generic_qed state =
    4.65 +  let val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state in
    4.66 +    state
    4.67 +    |> close_block
    4.68 +    |> `(fn outer_state =>
    4.69 +      let
    4.70 +        val results =
    4.71 +          tl (conclude_goal goal_ctxt goal stmt)
    4.72 +          |> burrow (Proof_Context.export goal_ctxt (context_of outer_state));
    4.73 +      in (after_qed, results) end)
    4.74    end;
    4.75  
    4.76  end;
    4.77 @@ -978,6 +966,18 @@
    4.78  
    4.79  (* local goals *)
    4.80  
    4.81 +local
    4.82 +
    4.83 +fun export_binds ctxt' ctxt binds =
    4.84 +  let
    4.85 +    val rhss =
    4.86 +      map (the_list o snd) binds
    4.87 +      |> burrow (Variable.export_terms ctxt' ctxt)
    4.88 +      |> map (try the_single);
    4.89 +  in map fst binds ~~ rhss end;
    4.90 +
    4.91 +in
    4.92 +
    4.93  fun local_goal print_results prep_att prep_propp prep_var
    4.94      kind before_qed after_qed fixes stmt state =
    4.95    let
    4.96 @@ -991,16 +991,28 @@
    4.97            |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
    4.98  
    4.99          val (propss, binds) = prep_propp fix_ctxt propp;
   4.100 +        val props = flat propss;
   4.101 +
   4.102          val (ps, params_ctxt) = fix_ctxt
   4.103 -          |> (fold o fold) Variable.declare_term propss
   4.104 -          |> Proof_Context.bind_terms binds
   4.105 +          |> fold Variable.declare_term props
   4.106 +          |> fold Variable.bind_term binds
   4.107            |> fold_map Proof_Context.inferred_param xs';
   4.108  
   4.109          val xs = map (Variable.check_name o #1) vars;
   4.110          val params = xs ~~ map Free ps;
   4.111  
   4.112 +        val binds' =
   4.113 +          (case try List.last props of
   4.114 +            NONE => []
   4.115 +          | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds);
   4.116 +        val result_binds =
   4.117 +          (Auto_Bind.facts params_ctxt props @ binds')
   4.118 +          |> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params)
   4.119 +          |> export_binds params_ctxt ctxt;
   4.120 +
   4.121          val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
   4.122 -      in ((propss, params, binds), params_ctxt) end;
   4.123 +
   4.124 +      in ((propss, result_binds), params_ctxt) end;
   4.125  
   4.126      fun after_qed' results =
   4.127        local_results ((names ~~ attss) ~~ results)
   4.128 @@ -1008,10 +1020,11 @@
   4.129        #> after_qed results;
   4.130    in generic_goal kind before_qed (after_qed', K I) make_statement state end;
   4.131  
   4.132 +end;
   4.133 +
   4.134  fun local_qeds arg =
   4.135    end_proof false arg
   4.136 -  #> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #->
   4.137 -    (fn ((after_qed, _), results) => after_qed results));
   4.138 +  #> Seq.map_result (generic_qed #-> (fn ((after_qed, _), results) => after_qed results));
   4.139  
   4.140  fun local_qed arg =
   4.141    local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
   4.142 @@ -1027,8 +1040,8 @@
   4.143            prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) propp;
   4.144          val ctxt' = ctxt
   4.145            |> (fold o fold) Variable.auto_fixes propss
   4.146 -          |> Proof_Context.bind_terms binds;
   4.147 -      in ((propss, [], []), ctxt') end;
   4.148 +          |> fold Variable.bind_term binds;
   4.149 +      in ((propss, []), ctxt') end;
   4.150    in init #> generic_goal "" before_qed (K I, after_qed) make_statement end;
   4.151  
   4.152  val theorem = global_goal Proof_Context.cert_propp;
   4.153 @@ -1036,7 +1049,7 @@
   4.154  
   4.155  fun global_qeds arg =
   4.156    end_proof true arg
   4.157 -  #> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
   4.158 +  #> Seq.map_result (generic_qed #> (fn (((_, after_qed), results), state) =>
   4.159      after_qed results (context_of state)));
   4.160  
   4.161  fun global_qed arg =
     5.1 --- a/src/Pure/Isar/proof_context.ML	Tue Jun 09 16:42:17 2015 +0200
     5.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Jun 09 22:24:33 2015 +0200
     5.3 @@ -105,8 +105,6 @@
     5.4    val export: Proof.context -> Proof.context -> thm list -> thm list
     5.5    val export_morphism: Proof.context -> Proof.context -> morphism
     5.6    val norm_export_morphism: Proof.context -> Proof.context -> morphism
     5.7 -  val maybe_bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
     5.8 -  val bind_terms: (indexname * term) list -> Proof.context -> Proof.context
     5.9    val auto_bind_goal: term list -> Proof.context -> Proof.context
    5.10    val auto_bind_facts: term list -> Proof.context -> Proof.context
    5.11    val match_bind: bool -> (term list * term) list -> Proof.context ->
    5.12 @@ -815,26 +813,23 @@
    5.13    | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
    5.14  
    5.15  
    5.16 -(* bind_terms *)
    5.17 -
    5.18 -val maybe_bind_terms = fold (fn (xi, t) => fn ctxt =>
    5.19 -  ctxt
    5.20 -  |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t));
    5.21 -
    5.22 -val bind_terms = maybe_bind_terms o map (apsnd SOME);
    5.23 -
    5.24 -
    5.25  (* auto_bind *)
    5.26  
    5.27 -fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
    5.28 -  | drop_schematic b = b;
    5.29 -
    5.30 -fun auto_bind f ts ctxt = ctxt |> maybe_bind_terms (map drop_schematic (f ctxt ts));
    5.31 +fun auto_bind f props ctxt = fold Variable.maybe_bind_term (f ctxt props) ctxt;
    5.32  
    5.33  val auto_bind_goal = auto_bind Auto_Bind.goal;
    5.34  val auto_bind_facts = auto_bind Auto_Bind.facts;
    5.35  
    5.36  
    5.37 +(* bind terms (non-schematic) *)
    5.38 +
    5.39 +fun cert_maybe_bind_term (xi, t) ctxt =
    5.40 +  ctxt
    5.41 +  |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t);
    5.42 +
    5.43 +val cert_bind_term = cert_maybe_bind_term o apsnd SOME;
    5.44 +
    5.45 +
    5.46  (* match_bind *)
    5.47  
    5.48  local
    5.49 @@ -857,8 +852,10 @@
    5.50      val ctxt'' =
    5.51        tap (Variable.warn_extra_tfrees ctxt)
    5.52         (if gen then
    5.53 -          ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> bind_terms binds'
    5.54 -        else ctxt' |> bind_terms binds');
    5.55 +          ctxt (*sic!*)
    5.56 +          |> fold Variable.declare_term (map #2 binds')
    5.57 +          |> fold cert_bind_term binds'
    5.58 +        else ctxt' |> fold cert_bind_term binds');
    5.59    in (ts, ctxt'') end;
    5.60  
    5.61  in
    5.62 @@ -1161,7 +1158,7 @@
    5.63      |> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss
    5.64      |-> (fn premss =>
    5.65        auto_bind_facts props
    5.66 -      #> bind_terms binds
    5.67 +      #> fold Variable.bind_term binds
    5.68        #> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss))
    5.69    end;
    5.70  
    5.71 @@ -1182,6 +1179,9 @@
    5.72  
    5.73  local
    5.74  
    5.75 +fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
    5.76 +  | drop_schematic b = b;
    5.77 +
    5.78  fun update_case _ _ ("", _) res = res
    5.79    | update_case _ _ (name, NONE) (cases, index) =
    5.80        (Name_Space.del_table name cases, index)
    5.81 @@ -1213,7 +1213,7 @@
    5.82      val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
    5.83    in
    5.84      ctxt'
    5.85 -    |> maybe_bind_terms (map drop_schematic binds)
    5.86 +    |> fold (cert_maybe_bind_term o drop_schematic) binds
    5.87      |> update_cases true (map (apsnd SOME) cases)
    5.88      |> pair (assumes, (binds, cases))
    5.89    end;