src/Pure/Isar/rule_insts.ML
changeset 27245 817d34377170
parent 27236 80356567e7ad
child 27282 432a5baa7546
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Mon Jun 16 22:13:52 2008 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Mon Jun 16 22:13:54 2008 +0200
     1.3 @@ -5,16 +5,24 @@
     1.4  Rule instantiations -- operations within a rule/subgoal context.
     1.5  *)
     1.6  
     1.7 -signature RULE_INSTS =
     1.8 +signature BASIC_RULE_INSTS =
     1.9  sig
    1.10    val read_instantiate: Proof.context -> (indexname * string) list -> thm -> thm
    1.11 -  val bires_inst_tac: bool -> Proof.context -> (indexname * string) list ->
    1.12 -    thm -> int -> tactic
    1.13 +  val instantiate_tac: Proof.context -> (indexname * string) list -> tactic
    1.14    val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    1.15    val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    1.16 +  val cut_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    1.17 +  val forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    1.18 +  val dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    1.19 +  val thin_tac: Proof.context -> string -> int -> tactic
    1.20    val subgoal_tac: Proof.context -> string -> int -> tactic
    1.21    val subgoals_tac: Proof.context -> string list -> int -> tactic
    1.22 -  val thin_tac: Proof.context -> string -> int -> tactic
    1.23 +end;
    1.24 +
    1.25 +signature RULE_INSTS =
    1.26 +sig
    1.27 +  include BASIC_RULE_INSTS
    1.28 +  val make_elim_preserve: thm -> thm
    1.29  end;
    1.30  
    1.31  structure RuleInsts: RULE_INSTS =
    1.32 @@ -173,11 +181,16 @@
    1.33        zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
    1.34    in read_instantiate_mixed ctxt insts thm end;
    1.35  
    1.36 +end;
    1.37 +
    1.38 +
    1.39 +(* instantiation of rule or goal state *)
    1.40 +
    1.41  fun read_instantiate ctxt args thm =
    1.42    read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic)  (* FIXME !? *)
    1.43      (map (fn (x, y) => (Args.eof, (x, Args.Text y))) args) thm;
    1.44  
    1.45 -end;
    1.46 +fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
    1.47  
    1.48  
    1.49  
    1.50 @@ -235,9 +248,11 @@
    1.51  
    1.52  
    1.53  
    1.54 -(** methods **)
    1.55 +(** tactics **)
    1.56  
    1.57 -(* rule_tac etc. -- refer to dynamic goal state!! *)   (* FIXME cleanup this mess!!! *)
    1.58 +(* resolution after lifting and instantation; may refer to parameters of the subgoal *)
    1.59 +
    1.60 +(* FIXME cleanup this mess!!! *)
    1.61  
    1.62  fun bires_inst_tac bires_flag ctxt insts thm =
    1.63    let
    1.64 @@ -320,6 +335,47 @@
    1.65  val eres_inst_tac = bires_inst_tac true;
    1.66  
    1.67  
    1.68 +(* forward resolution *)
    1.69 +
    1.70 +fun make_elim_preserve rl =
    1.71 +  let
    1.72 +    val cert = Thm.cterm_of (Thm.theory_of_thm rl);
    1.73 +    val maxidx = Thm.maxidx_of rl;
    1.74 +    fun cvar xi = cert (Var (xi, propT));
    1.75 +    val revcut_rl' =
    1.76 +      instantiate ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
    1.77 +        (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
    1.78 +  in
    1.79 +    (case Seq.list_of (bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
    1.80 +      [th] => th
    1.81 +    | _ => raise THM ("make_elim_preserve", 1, [rl]))
    1.82 +  end;
    1.83 +
    1.84 +(*instantiate and cut -- for atomic fact*)
    1.85 +fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve rule);
    1.86 +
    1.87 +(*forward tactic applies a rule to an assumption without deleting it*)
    1.88 +fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac;
    1.89 +
    1.90 +(*dresolve tactic applies a rule to replace an assumption*)
    1.91 +fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve rule);
    1.92 +
    1.93 +
    1.94 +(* derived tactics *)
    1.95 +
    1.96 +(*deletion of an assumption*)
    1.97 +fun thin_tac ctxt s = eres_inst_tac ctxt [(("V", 0), s)] Drule.thin_rl;
    1.98 +
    1.99 +(*Introduce the given proposition as lemma and subgoal*)
   1.100 +fun subgoal_tac ctxt A = DETERM o res_inst_tac ctxt [(("psi", 0), A)] cut_rl;
   1.101 +fun subgoals_tac ctxt As = EVERY' (map (subgoal_tac ctxt) As);
   1.102 +
   1.103 +
   1.104 +
   1.105 +(** methods **)
   1.106 +
   1.107 +(* rule_tac etc. -- refer to dynamic goal state! *)
   1.108 +
   1.109  local
   1.110  
   1.111  fun gen_inst _ tac _ (quant, ([], thms)) =
   1.112 @@ -333,27 +389,11 @@
   1.113  
   1.114  val res_inst_meth = gen_inst res_inst_tac Tactic.resolve_tac;
   1.115  val eres_inst_meth = gen_inst eres_inst_tac Tactic.eresolve_tac;
   1.116 -
   1.117 -val cut_inst_meth =
   1.118 -  gen_inst
   1.119 -    (fn ctxt => fn insts => res_inst_tac ctxt insts o Tactic.make_elim_preserve)
   1.120 -    Tactic.cut_rules_tac;
   1.121 -
   1.122 -val dres_inst_meth =
   1.123 -  gen_inst
   1.124 -    (fn ctxt => fn insts => eres_inst_tac ctxt insts o Tactic.make_elim_preserve)
   1.125 -    Tactic.dresolve_tac;
   1.126 +val cut_inst_meth = gen_inst cut_inst_tac Tactic.cut_rules_tac;
   1.127 +val dres_inst_meth = gen_inst dres_inst_tac Tactic.dresolve_tac;
   1.128 +val forw_inst_meth = gen_inst forw_inst_tac Tactic.forward_tac;
   1.129  
   1.130 -val forw_inst_meth =
   1.131 -  gen_inst
   1.132 -    (fn ctxt => fn insts => fn rule =>
   1.133 -       res_inst_tac ctxt insts (Tactic.make_elim_preserve rule) THEN' assume_tac)
   1.134 -    Tactic.forward_tac;
   1.135 -
   1.136 -fun subgoal_tac ctxt sprop = DETERM o res_inst_tac ctxt [(("psi", 0), sprop)] cut_rl;
   1.137 -fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops);
   1.138 -
   1.139 -fun thin_tac ctxt s = eres_inst_tac ctxt [(("V", 0), s)] thin_rl;
   1.140 +end;
   1.141  
   1.142  
   1.143  (* method syntax *)
   1.144 @@ -396,4 +436,6 @@
   1.145  
   1.146  end;
   1.147  
   1.148 -end;
   1.149 +structure BasicRuleInsts: BASIC_RULE_INSTS = RuleInsts;
   1.150 +open BasicRuleInsts;
   1.151 +