src/Pure/Tools/rule_insts.ML
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 63120 629a4c5e953e
child 67147 dea94b1aabc3
permissions -rw-r--r--
tuned signature;
wenzelm@53707
     1
(*  Title:      Pure/Tools/rule_insts.ML
wenzelm@20336
     2
    Author:     Makarius
wenzelm@20336
     3
wenzelm@53708
     4
Rule instantiations -- operations within implicit rule / subgoal context.
wenzelm@20336
     5
*)
wenzelm@20336
     6
wenzelm@59763
     7
signature RULE_INSTS =
wenzelm@20336
     8
sig
wenzelm@59763
     9
  val where_rule: Proof.context ->
wenzelm@59763
    10
    ((indexname * Position.T) * string) list ->
wenzelm@59763
    11
    (binding * string option * mixfix) list -> thm -> thm
wenzelm@59763
    12
  val of_rule: Proof.context -> string option list * string option list ->
wenzelm@59763
    13
    (binding * string option * mixfix) list -> thm -> thm
wenzelm@59763
    14
  val read_instantiate: Proof.context ->
wenzelm@59763
    15
    ((indexname * Position.T) * string) list -> string list -> thm -> thm
wenzelm@59827
    16
  val read_term: string -> Proof.context -> term * Proof.context
wenzelm@59829
    17
  val goal_context: term -> Proof.context -> (string * typ) list * Proof.context
wenzelm@59755
    18
  val res_inst_tac: Proof.context ->
wenzelm@59855
    19
    ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
wenzelm@59855
    20
    thm -> int -> tactic
wenzelm@59755
    21
  val eres_inst_tac: Proof.context ->
wenzelm@59855
    22
    ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
wenzelm@59855
    23
    thm -> int -> tactic
wenzelm@59755
    24
  val cut_inst_tac: Proof.context ->
wenzelm@59855
    25
    ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
wenzelm@59855
    26
    thm -> int -> tactic
wenzelm@59755
    27
  val forw_inst_tac: Proof.context ->
wenzelm@59855
    28
    ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
wenzelm@59855
    29
    thm -> int -> tactic
wenzelm@59755
    30
  val dres_inst_tac: Proof.context ->
wenzelm@59855
    31
    ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
wenzelm@59855
    32
    thm -> int -> tactic
wenzelm@59780
    33
  val thin_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
wenzelm@59780
    34
    int -> tactic
wenzelm@59780
    35
  val subgoal_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
wenzelm@59780
    36
    int -> tactic
wenzelm@58950
    37
  val make_elim_preserve: Proof.context -> thm -> thm
wenzelm@59755
    38
  val method:
wenzelm@59780
    39
    (Proof.context -> ((indexname * Position.T) * string) list ->
wenzelm@59780
    40
      (binding * string option * mixfix) list -> thm -> int -> tactic) ->
wenzelm@59855
    41
    (Proof.context -> thm list -> int -> tactic) ->
wenzelm@59855
    42
    (Proof.context -> Proof.method) context_parser
wenzelm@20336
    43
end;
wenzelm@20336
    44
wenzelm@42806
    45
structure Rule_Insts: RULE_INSTS =
wenzelm@20336
    46
struct
wenzelm@20336
    47
wenzelm@59771
    48
(** read instantiations **)
wenzelm@20336
    49
wenzelm@59771
    50
local
wenzelm@59755
    51
wenzelm@59755
    52
fun error_var msg (xi, pos) =
wenzelm@59755
    53
  error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos);
wenzelm@59754
    54
wenzelm@59755
    55
fun the_sort tvars (xi, pos) : sort =
wenzelm@45611
    56
  (case AList.lookup (op =) tvars xi of
wenzelm@45611
    57
    SOME S => S
wenzelm@59755
    58
  | NONE => error_var "No such type variable in theorem: " (xi, pos));
wenzelm@20336
    59
wenzelm@59755
    60
fun the_type vars (xi, pos) : typ =
wenzelm@45611
    61
  (case AList.lookup (op =) vars xi of
wenzelm@45611
    62
    SOME T => T
wenzelm@59755
    63
  | NONE => error_var "No such variable in theorem: " (xi, pos));
wenzelm@20336
    64
wenzelm@59774
    65
fun read_type ctxt tvars ((xi, pos), s) =
wenzelm@59759
    66
  let
wenzelm@59759
    67
    val S = the_sort tvars (xi, pos);
wenzelm@59759
    68
    val T = Syntax.read_typ ctxt s;
wenzelm@59759
    69
  in
wenzelm@59759
    70
    if Sign.of_sort (Proof_Context.theory_of ctxt) (T, S) then ((xi, S), T)
wenzelm@59768
    71
    else error_var "Bad sort for instantiation of type variable: " (xi, pos)
wenzelm@59759
    72
  end;
wenzelm@59759
    73
wenzelm@59827
    74
fun make_instT f v =
wenzelm@59827
    75
  let
wenzelm@59827
    76
    val T = TVar v;
wenzelm@59827
    77
    val T' = f T;
wenzelm@59827
    78
  in if T = T' then NONE else SOME (v, T') end;
wenzelm@59827
    79
wenzelm@59827
    80
fun make_inst f v =
wenzelm@59827
    81
  let
wenzelm@59827
    82
    val t = Var v;
wenzelm@59827
    83
    val t' = f t;
wenzelm@59827
    84
  in if t aconv t' then NONE else SOME (v, t') end;
wenzelm@59827
    85
wenzelm@59796
    86
fun read_terms ss Ts ctxt =
wenzelm@25329
    87
  let
wenzelm@25329
    88
    fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
wenzelm@59796
    89
    val (ts, ctxt') = fold_map Variable.fix_dummy_patterns (map2 parse Ts ss) ctxt;
wenzelm@25329
    90
    val ts' =
wenzelm@39288
    91
      map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
wenzelm@59796
    92
      |> Syntax.check_terms ctxt'
wenzelm@59796
    93
      |> Variable.polymorphic ctxt';
wenzelm@25329
    94
    val Ts' = map Term.fastype_of ts';
wenzelm@59839
    95
    val tyenv = fold (Sign.typ_match (Proof_Context.theory_of ctxt)) (Ts ~~ Ts') Vartab.empty;
wenzelm@59759
    96
    val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
wenzelm@59796
    97
  in ((ts', tyenv'), ctxt') end;
wenzelm@25329
    98
wenzelm@59827
    99
in
wenzelm@59771
   100
wenzelm@59827
   101
fun read_term s ctxt =
wenzelm@59771
   102
  let
wenzelm@59827
   103
    val (t, ctxt') = Variable.fix_dummy_patterns (Syntax.parse_term ctxt s) ctxt;
wenzelm@59827
   104
    val t' = Syntax.check_term ctxt' t;
wenzelm@59827
   105
  in (t', ctxt') end;
wenzelm@59771
   106
wenzelm@59853
   107
fun read_insts thm raw_insts raw_fixes ctxt =
wenzelm@20336
   108
  let
wenzelm@59771
   109
    val (type_insts, term_insts) =
wenzelm@59853
   110
      List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) raw_insts;
wenzelm@59768
   111
wenzelm@59769
   112
    val tvars = Thm.fold_terms Term.add_tvars thm [];
wenzelm@59769
   113
    val vars = Thm.fold_terms Term.add_vars thm [];
wenzelm@20336
   114
wenzelm@59853
   115
    (*eigen-context*)
wenzelm@60469
   116
    val (_, ctxt1) = ctxt
wenzelm@62012
   117
      |> fold (Variable.declare_internal o Logic.mk_type o TVar) tvars
wenzelm@62012
   118
      |> fold (Variable.declare_internal o Var) vars
wenzelm@60469
   119
      |> Proof_Context.add_fixes_cmd raw_fixes;
wenzelm@59853
   120
wenzelm@59771
   121
    (*explicit type instantiations*)
wenzelm@59825
   122
    val instT1 = Term_Subst.instantiateT (map (read_type ctxt1 tvars) type_insts);
wenzelm@20343
   123
    val vars1 = map (apsnd instT1) vars;
wenzelm@20336
   124
wenzelm@59771
   125
    (*term instantiations*)
wenzelm@45613
   126
    val (xs, ss) = split_list term_insts;
wenzelm@45613
   127
    val Ts = map (the_type vars1) xs;
wenzelm@59825
   128
    val ((ts, inferred), ctxt2) = read_terms ss Ts ctxt1;
wenzelm@45613
   129
wenzelm@59771
   130
    (*implicit type instantiations*)
wenzelm@59759
   131
    val instT2 = Term_Subst.instantiateT inferred;
wenzelm@20343
   132
    val vars2 = map (apsnd instT2) vars1;
wenzelm@59774
   133
    val inst2 =
wenzelm@59774
   134
      Term_Subst.instantiate ([], map2 (fn (xi, _) => fn t => ((xi, Term.fastype_of t), t)) xs ts)
wenzelm@59774
   135
      #> Envir.beta_norm;
wenzelm@20336
   136
wenzelm@45613
   137
    val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
wenzelm@45613
   138
    val inst_vars = map_filter (make_inst inst2) vars2;
wenzelm@59825
   139
  in ((inst_tvars, inst_vars), ctxt2) end;
wenzelm@20343
   140
wenzelm@59771
   141
end;
wenzelm@59771
   142
wenzelm@59771
   143
wenzelm@59771
   144
wenzelm@59771
   145
(** forward rules **)
wenzelm@59771
   146
wenzelm@59853
   147
fun where_rule ctxt raw_insts raw_fixes thm =
wenzelm@20343
   148
  let
wenzelm@59853
   149
    val ((inst_tvars, inst_vars), ctxt') = read_insts thm raw_insts raw_fixes ctxt;
wenzelm@20343
   150
  in
wenzelm@59769
   151
    thm
wenzelm@59769
   152
    |> Drule.instantiate_normalize
wenzelm@60642
   153
      (map (apsnd (Thm.ctyp_of ctxt')) inst_tvars,
wenzelm@60642
   154
       map (apsnd (Thm.cterm_of ctxt')) inst_vars)
wenzelm@59853
   155
    |> singleton (Variable.export ctxt' ctxt)
wenzelm@45613
   156
    |> Rule_Cases.save thm
wenzelm@20343
   157
  end;
wenzelm@20336
   158
wenzelm@55143
   159
fun of_rule ctxt (args, concl_args) fixes thm =
wenzelm@20343
   160
  let
wenzelm@20343
   161
    fun zip_vars _ [] = []
wenzelm@45613
   162
      | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
wenzelm@59755
   163
      | zip_vars ((x, _) :: xs) (SOME t :: rest) = ((x, Position.none), t) :: zip_vars xs rest
wenzelm@20343
   164
      | zip_vars [] _ = error "More instantiations than variables in theorem";
wenzelm@20343
   165
    val insts =
wenzelm@20343
   166
      zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
wenzelm@20343
   167
      zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
wenzelm@55143
   168
  in where_rule ctxt insts fixes thm end;
wenzelm@27236
   169
wenzelm@55143
   170
fun read_instantiate ctxt insts xs =
wenzelm@55143
   171
  where_rule ctxt insts (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
wenzelm@20336
   172
wenzelm@20336
   173
wenzelm@20343
   174
wenzelm@20343
   175
(** attributes **)
wenzelm@20343
   176
wenzelm@20336
   177
(* where: named instantiation *)
wenzelm@20336
   178
wenzelm@59855
   179
val named_insts =
wenzelm@63120
   180
  Parse.and_list1
wenzelm@63120
   181
    (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.embedded_inner_syntax))
wenzelm@59853
   182
    -- Parse.for_fixes;
wenzelm@59853
   183
wenzelm@53171
   184
val _ = Theory.setup
wenzelm@53708
   185
  (Attrib.setup @{binding "where"}
wenzelm@59855
   186
    (Scan.lift named_insts >> (fn args =>
wenzelm@61853
   187
      Thm.rule_attribute [] (fn context => uncurry (where_rule (Context.proof_of context)) args)))
wenzelm@53171
   188
    "named instantiation of theorem");
wenzelm@20336
   189
wenzelm@20336
   190
wenzelm@20343
   191
(* of: positional instantiation (terms only) *)
wenzelm@20336
   192
wenzelm@20336
   193
local
wenzelm@20336
   194
wenzelm@63120
   195
val inst = Args.maybe Args.embedded_inner_syntax;
wenzelm@20336
   196
val concl = Args.$$$ "concl" -- Args.colon;
wenzelm@20336
   197
wenzelm@20336
   198
val insts =
wenzelm@20336
   199
  Scan.repeat (Scan.unless concl inst) --
wenzelm@20336
   200
  Scan.optional (concl |-- Scan.repeat inst) [];
wenzelm@20336
   201
wenzelm@20336
   202
in
wenzelm@20336
   203
wenzelm@53171
   204
val _ = Theory.setup
wenzelm@53708
   205
  (Attrib.setup @{binding "of"}
wenzelm@59855
   206
    (Scan.lift (insts -- Parse.for_fixes) >> (fn args =>
wenzelm@61853
   207
      Thm.rule_attribute [] (fn context => uncurry (of_rule (Context.proof_of context)) args)))
wenzelm@53171
   208
    "positional instantiation of theorem");
wenzelm@20336
   209
wenzelm@20336
   210
end;
wenzelm@20336
   211
wenzelm@20336
   212
wenzelm@20336
   213
wenzelm@27245
   214
(** tactics **)
wenzelm@20336
   215
wenzelm@59825
   216
(* goal context *)
wenzelm@59825
   217
wenzelm@59829
   218
fun goal_context goal ctxt =
wenzelm@20336
   219
  let
wenzelm@59828
   220
    val ((_, params), ctxt') = ctxt
wenzelm@59829
   221
      |> Variable.declare_constraints goal
wenzelm@59790
   222
      |> Variable.improper_fixes
wenzelm@60695
   223
      |> Variable.focus_params NONE goal
wenzelm@60331
   224
      ||> Variable.restore_proper_fixes ctxt;
wenzelm@59828
   225
  in (params, ctxt') end;
wenzelm@59825
   226
wenzelm@59825
   227
wenzelm@59825
   228
(* resolution after lifting and instantiation; may refer to parameters of the subgoal *)
wenzelm@59825
   229
wenzelm@59853
   230
fun bires_inst_tac bires_flag ctxt raw_insts raw_fixes thm i st = CSUBGOAL (fn (cgoal, _) =>
wenzelm@59825
   231
  let
wenzelm@59855
   232
    (*goal context*)
wenzelm@59834
   233
    val (params, goal_ctxt) = goal_context (Thm.term_of cgoal) ctxt;
wenzelm@59825
   234
    val paramTs = map #2 params;
wenzelm@59754
   235
wenzelm@59855
   236
    (*instantiation context*)
wenzelm@59853
   237
    val ((inst_tvars, inst_vars), inst_ctxt) = read_insts thm raw_insts raw_fixes goal_ctxt;
wenzelm@59846
   238
    val fixed = map #1 (fold (Variable.add_newly_fixed inst_ctxt goal_ctxt o #2) inst_vars []);
wenzelm@59805
   239
wenzelm@59780
   240
wenzelm@59780
   241
    (* lift and instantiate rule *)
wenzelm@59754
   242
wenzelm@59774
   243
    val inc = Thm.maxidx_of st + 1;
wenzelm@59825
   244
    val lift_type = Logic.incr_tvar inc;
wenzelm@60642
   245
    fun lift_var ((a, j), T) = ((a, j + inc), paramTs ---> lift_type T);
wenzelm@59825
   246
    fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t);
wenzelm@59754
   247
wenzelm@59771
   248
    val inst_tvars' = inst_tvars
wenzelm@60642
   249
      |> map (fn (((a, i), S), T) => (((a, i + inc), S), Thm.ctyp_of inst_ctxt (lift_type T)));
wenzelm@59771
   250
    val inst_vars' = inst_vars
wenzelm@60642
   251
      |> map (fn (v, t) => (lift_var v, Thm.cterm_of inst_ctxt (lift_term t)));
wenzelm@59771
   252
wenzelm@59825
   253
    val thm' = Thm.lift_rule cgoal thm
wenzelm@59825
   254
      |> Drule.instantiate_normalize (inst_tvars', inst_vars')
wenzelm@59836
   255
      |> singleton (Variable.export inst_ctxt ctxt);
wenzelm@59836
   256
  in compose_tac ctxt (bires_flag, thm', Thm.nprems_of thm) i end) i st;
wenzelm@20336
   257
wenzelm@27120
   258
val res_inst_tac = bires_inst_tac false;
wenzelm@27120
   259
val eres_inst_tac = bires_inst_tac true;
wenzelm@27120
   260
wenzelm@27120
   261
wenzelm@27245
   262
(* forward resolution *)
wenzelm@27245
   263
wenzelm@58950
   264
fun make_elim_preserve ctxt rl =
wenzelm@27245
   265
  let
wenzelm@27245
   266
    val maxidx = Thm.maxidx_of rl;
wenzelm@60642
   267
    fun var x = ((x, 0), propT);
wenzelm@59623
   268
    fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT));
wenzelm@27245
   269
    val revcut_rl' =
wenzelm@60642
   270
      Drule.instantiate_normalize ([], [(var "V", cvar ("V", maxidx + 1)),
wenzelm@60642
   271
        (var "W", cvar ("W", maxidx + 1))]) Drule.revcut_rl;
wenzelm@27245
   272
  in
wenzelm@52223
   273
    (case Seq.list_of
wenzelm@58950
   274
      (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}
wenzelm@52223
   275
        (false, rl, Thm.nprems_of rl) 1 revcut_rl')
wenzelm@52223
   276
     of
wenzelm@27245
   277
      [th] => th
wenzelm@27245
   278
    | _ => raise THM ("make_elim_preserve", 1, [rl]))
wenzelm@27245
   279
  end;
wenzelm@27245
   280
wenzelm@27245
   281
(*instantiate and cut -- for atomic fact*)
wenzelm@59780
   282
fun cut_inst_tac ctxt insts fixes rule =
wenzelm@59780
   283
  res_inst_tac ctxt insts fixes (make_elim_preserve ctxt rule);
wenzelm@27245
   284
wenzelm@27245
   285
(*forward tactic applies a rule to an assumption without deleting it*)
wenzelm@59780
   286
fun forw_inst_tac ctxt insts fixes rule =
wenzelm@59780
   287
  cut_inst_tac ctxt insts fixes rule THEN' assume_tac ctxt;
wenzelm@27245
   288
wenzelm@27245
   289
(*dresolve tactic applies a rule to replace an assumption*)
wenzelm@59780
   290
fun dres_inst_tac ctxt insts fixes rule =
wenzelm@59780
   291
  eres_inst_tac ctxt insts fixes (make_elim_preserve ctxt rule);
wenzelm@27245
   292
wenzelm@27245
   293
wenzelm@27245
   294
(* derived tactics *)
wenzelm@27245
   295
wenzelm@27245
   296
(*deletion of an assumption*)
wenzelm@59780
   297
fun thin_tac ctxt s fixes =
wenzelm@59780
   298
  eres_inst_tac ctxt [((("V", 0), Position.none), s)] fixes Drule.thin_rl;
wenzelm@27245
   299
wenzelm@27245
   300
(*Introduce the given proposition as lemma and subgoal*)
wenzelm@59780
   301
fun subgoal_tac ctxt A fixes =
wenzelm@59780
   302
  DETERM o res_inst_tac ctxt [((("psi", 0), Position.none), A)] fixes cut_rl;
wenzelm@27245
   303
wenzelm@27245
   304
wenzelm@53708
   305
(* method wrapper *)
wenzelm@27245
   306
wenzelm@30545
   307
fun method inst_tac tac =
wenzelm@59855
   308
  Args.goal_spec -- Scan.optional (Scan.lift (named_insts --| Args.$$$ "in")) ([], []) --
wenzelm@59855
   309
  Attrib.thms >> (fn ((quant, (insts, fixes)), thms) => fn ctxt => METHOD (fn facts =>
wenzelm@59780
   310
    if null insts andalso null fixes
wenzelm@61841
   311
    then quant (Method.insert_tac ctxt facts THEN' tac ctxt thms)
wenzelm@30515
   312
    else
wenzelm@30515
   313
      (case thms of
wenzelm@61841
   314
        [thm] => quant (Method.insert_tac ctxt facts THEN' inst_tac ctxt insts fixes thm)
wenzelm@30515
   315
      | _ => error "Cannot have instantiations with multiple rules")));
wenzelm@20336
   316
wenzelm@20336
   317
wenzelm@20336
   318
(* setup *)
wenzelm@20336
   319
wenzelm@53708
   320
(*warning: rule_tac etc. refer to dynamic subgoal context!*)
wenzelm@53708
   321
wenzelm@53171
   322
val _ = Theory.setup
wenzelm@59498
   323
 (Method.setup @{binding rule_tac} (method res_inst_tac resolve_tac)
wenzelm@53708
   324
    "apply rule (dynamic instantiation)" #>
wenzelm@59498
   325
  Method.setup @{binding erule_tac} (method eres_inst_tac eresolve_tac)
wenzelm@30515
   326
    "apply rule in elimination manner (dynamic instantiation)" #>
wenzelm@59498
   327
  Method.setup @{binding drule_tac} (method dres_inst_tac dresolve_tac)
wenzelm@30515
   328
    "apply rule in destruct manner (dynamic instantiation)" #>
wenzelm@59498
   329
  Method.setup @{binding frule_tac} (method forw_inst_tac forward_tac)
wenzelm@30515
   330
    "apply rule in forward manner (dynamic instantiation)" #>
wenzelm@53708
   331
  Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
wenzelm@53708
   332
    "cut rule (dynamic instantiation)" #>
wenzelm@53708
   333
  Method.setup @{binding subgoal_tac}
wenzelm@63120
   334
    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.embedded_inner_syntax -- Parse.for_fixes) >>
wenzelm@59780
   335
      (fn (quant, (props, fixes)) => fn ctxt =>
wenzelm@59780
   336
        SIMPLE_METHOD'' quant (EVERY' (map (fn prop => subgoal_tac ctxt prop fixes) props))))
wenzelm@30515
   337
    "insert subgoal (dynamic instantiation)" #>
wenzelm@53708
   338
  Method.setup @{binding thin_tac}
wenzelm@63120
   339
    (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
wenzelm@59780
   340
      (fn (quant, (prop, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop fixes)))
wenzelm@59780
   341
    "remove premise (dynamic instantiation)");
wenzelm@20336
   342
wenzelm@20336
   343
end;