moved bires_inst_tac etc. to rule_insts.ML;
authorwenzelm
Thu Aug 03 17:30:43 2006 +0200 (2006-08-03)
changeset 20335b5eca86ef9cc
parent 20334 60157137a0eb
child 20336 aac494583949
moved bires_inst_tac etc. to rule_insts.ML;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Thu Aug 03 17:30:42 2006 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Aug 03 17:30:43 2006 +0200
     1.3 @@ -50,8 +50,6 @@
     1.4    val drule: int -> thm list -> method
     1.5    val frule: int -> thm list -> method
     1.6    val iprover_tac: Proof.context -> int option -> int -> tactic
     1.7 -  val bires_inst_tac: bool -> Proof.context -> (indexname * string) list ->
     1.8 -    thm -> int -> tactic
     1.9    val set_tactic: (Proof.context -> thm list -> tactic) -> unit
    1.10    val tactic: string -> Proof.context -> method
    1.11    type src
    1.12 @@ -337,134 +335,6 @@
    1.13  end;
    1.14  
    1.15  
    1.16 -(* rule_tac etc. -- refer to dynamic goal state!! *)   (* FIXME cleanup!! *)
    1.17 -
    1.18 -fun bires_inst_tac bires_flag ctxt insts thm =
    1.19 -  let
    1.20 -    val thy = ProofContext.theory_of ctxt;
    1.21 -    (* Separate type and term insts *)
    1.22 -    fun has_type_var ((x, _), _) = (case Symbol.explode x of
    1.23 -          "'"::cs => true | cs => false);
    1.24 -    val Tinsts = List.filter has_type_var insts;
    1.25 -    val tinsts = filter_out has_type_var insts;
    1.26 -    (* Tactic *)
    1.27 -    fun tac i st =
    1.28 -      let
    1.29 -        (* Preprocess state: extract environment information:
    1.30 -           - variables and their types
    1.31 -           - type variables and their sorts
    1.32 -           - parameters and their types *)
    1.33 -        val (types, sorts) = types_sorts st;
    1.34 -    (* Process type insts: Tinsts_env *)
    1.35 -    fun absent xi = error
    1.36 -          ("No such variable in theorem: " ^ Syntax.string_of_vname xi);
    1.37 -    val (rtypes, rsorts) = types_sorts thm;
    1.38 -    fun readT (xi, s) =
    1.39 -        let val S = case rsorts xi of SOME S => S | NONE => absent xi;
    1.40 -            val T = Sign.read_typ (thy, sorts) s;
    1.41 -            val U = TVar (xi, S);
    1.42 -        in if Sign.typ_instance thy (T, U) then (U, T)
    1.43 -           else error
    1.44 -             ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
    1.45 -        end;
    1.46 -    val Tinsts_env = map readT Tinsts;
    1.47 -    (* Preprocess rule: extract vars and their types, apply Tinsts *)
    1.48 -    fun get_typ xi =
    1.49 -      (case rtypes xi of
    1.50 -           SOME T => typ_subst_atomic Tinsts_env T
    1.51 -         | NONE => absent xi);
    1.52 -    val (xis, ss) = Library.split_list tinsts;
    1.53 -    val Ts = map get_typ xis;
    1.54 -        val (_, _, Bi, _) = dest_state(st,i)
    1.55 -        val params = Logic.strip_params Bi
    1.56 -                             (* params of subgoal i as string typ pairs *)
    1.57 -        val params = rev(Term.rename_wrt_term Bi params)
    1.58 -                           (* as they are printed: bound variables with *)
    1.59 -                           (* the same name are renamed during printing *)
    1.60 -        fun types' (a, ~1) = (case AList.lookup (op =) params a of
    1.61 -                NONE => types (a, ~1)
    1.62 -              | some => some)
    1.63 -          | types' xi = types xi;
    1.64 -        fun internal x = is_some (types' (x, ~1));
    1.65 -        val used = Drule.add_used thm (Drule.add_used st []);
    1.66 -        val (ts, envT) =
    1.67 -          ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts);
    1.68 -        val envT' = map (fn (ixn, T) =>
    1.69 -          (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
    1.70 -        val cenv =
    1.71 -          map
    1.72 -            (fn (xi, t) =>
    1.73 -              pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
    1.74 -            (distinct
    1.75 -              (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
    1.76 -              (xis ~~ ts));
    1.77 -        (* Lift and instantiate rule *)
    1.78 -        val {maxidx, ...} = rep_thm st;
    1.79 -        val paramTs = map #2 params
    1.80 -        and inc = maxidx+1
    1.81 -        fun liftvar (Var ((a,j), T)) =
    1.82 -              Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
    1.83 -          | liftvar t = raise TERM("Variable expected", [t]);
    1.84 -        fun liftterm t = list_abs_free
    1.85 -              (params, Logic.incr_indexes(paramTs,inc) t)
    1.86 -        fun liftpair (cv,ct) =
    1.87 -              (cterm_fun liftvar cv, cterm_fun liftterm ct)
    1.88 -        val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
    1.89 -        val rule = Drule.instantiate
    1.90 -              (map lifttvar envT', map liftpair cenv)
    1.91 -              (Thm.lift_rule (Thm.cprem_of st i) thm)
    1.92 -      in
    1.93 -        if i > nprems_of st then no_tac st
    1.94 -        else st |>
    1.95 -          compose_tac (bires_flag, rule, nprems_of thm) i
    1.96 -      end
    1.97 -           handle TERM (msg,_)   => (warning msg; no_tac st)
    1.98 -                | THM  (msg,_,_) => (warning msg; no_tac st);
    1.99 -  in tac end;
   1.100 -
   1.101 -local
   1.102 -
   1.103 -fun gen_inst _ tac _ (quant, ([], thms)) =
   1.104 -      METHOD (fn facts => quant (insert_tac facts THEN' tac thms))
   1.105 -  | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
   1.106 -      METHOD (fn facts =>
   1.107 -        quant (insert_tac facts THEN' inst_tac ctxt insts thm))
   1.108 -  | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
   1.109 -
   1.110 -in
   1.111 -
   1.112 -val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac;
   1.113 -
   1.114 -val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac;
   1.115 -
   1.116 -val cut_inst_meth =
   1.117 -  gen_inst
   1.118 -    (fn ctxt => fn insts => bires_inst_tac false ctxt insts o Tactic.make_elim_preserve)
   1.119 -    Tactic.cut_rules_tac;
   1.120 -
   1.121 -val dres_inst_meth =
   1.122 -  gen_inst
   1.123 -    (fn ctxt => fn insts => bires_inst_tac true ctxt insts o Tactic.make_elim_preserve)
   1.124 -    Tactic.dresolve_tac;
   1.125 -
   1.126 -val forw_inst_meth =
   1.127 -  gen_inst
   1.128 -    (fn ctxt => fn insts => fn rule =>
   1.129 -       bires_inst_tac false ctxt insts (Tactic.make_elim_preserve rule) THEN'
   1.130 -       assume_tac)
   1.131 -    Tactic.forward_tac;
   1.132 -
   1.133 -fun subgoal_tac ctxt sprop =
   1.134 -  DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl;
   1.135 -
   1.136 -fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops);
   1.137 -
   1.138 -fun thin_tac ctxt s =
   1.139 -  bires_inst_tac true ctxt [(("V", 0), s)] thin_rl;
   1.140 -
   1.141 -end;
   1.142 -
   1.143 -
   1.144  (* ML tactics *)
   1.145  
   1.146  val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
   1.147 @@ -670,21 +540,6 @@
   1.148  fun nat_thms_args f = uncurry f oo
   1.149    (#2 oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms));
   1.150  
   1.151 -val insts =
   1.152 -  Scan.optional
   1.153 -    (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
   1.154 -      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
   1.155 -
   1.156 -fun inst_args f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
   1.157 -
   1.158 -val insts_var =
   1.159 -  Scan.optional
   1.160 -    (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
   1.161 -      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
   1.162 -
   1.163 -fun inst_args_var f src ctxt =
   1.164 -  f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
   1.165 -
   1.166  fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >>
   1.167    (fn (quant, s) => SIMPLE_METHOD' quant (tac s))) src ctxt);
   1.168  
   1.169 @@ -697,14 +552,6 @@
   1.170  fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
   1.171  
   1.172  
   1.173 -(* misc tactic emulations *)
   1.174 -
   1.175 -val subgoal_meth = goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac;
   1.176 -val thin_meth = goal_args_ctxt Args.name thin_tac;
   1.177 -val rename_meth = goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac;
   1.178 -val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac;
   1.179 -
   1.180 -
   1.181  (* theory setup *)
   1.182  
   1.183  val _ = Context.add_setup (add_methods
   1.184 @@ -726,15 +573,10 @@
   1.185    ("this", no_args this, "apply current facts as rules"),
   1.186    ("fact", thms_ctxt_args fact, "composition by facts from context"),
   1.187    ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
   1.188 -  ("rule_tac", inst_args_var res_inst_meth, "apply rule (dynamic instantiation)"),
   1.189 -  ("erule_tac", inst_args_var eres_inst_meth, "apply rule in elimination manner (dynamic instantiation)"),
   1.190 -  ("drule_tac", inst_args_var dres_inst_meth, "apply rule in destruct manner (dynamic instantiation)"),
   1.191 -  ("frule_tac", inst_args_var forw_inst_meth, "apply rule in forward manner (dynamic instantiation)"),
   1.192 -  ("cut_tac", inst_args_var cut_inst_meth, "cut rule (dynamic instantiation)"),
   1.193 -  ("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation)"),
   1.194 -  ("thin_tac", thin_meth, "remove premise (dynamic instantiation)"),
   1.195 -  ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation)"),
   1.196 -  ("rotate_tac", rotate_meth, "rotate assumptions of goal"),
   1.197 +  ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac,
   1.198 +    "rename parameters of goal (dynamic instantiation)"),
   1.199 +  ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
   1.200 +    "rotate assumptions of goal"),
   1.201    ("tactic", simple_args Args.name tactic, "ML tactic as proof method")]);
   1.202  
   1.203