# HG changeset patch # User wenzelm # Date 1154619043 -7200 # Node ID b5eca86ef9cc4e2d2e48431418f522ff7111edfd # Parent 60157137a0eb5deaa15d6f4fd74e1fa8208a4552 moved bires_inst_tac etc. to rule_insts.ML; diff -r 60157137a0eb -r b5eca86ef9cc src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Aug 03 17:30:42 2006 +0200 +++ b/src/Pure/Isar/method.ML Thu Aug 03 17:30:43 2006 +0200 @@ -50,8 +50,6 @@ val drule: int -> thm list -> method val frule: int -> thm list -> method val iprover_tac: Proof.context -> int option -> int -> tactic - val bires_inst_tac: bool -> Proof.context -> (indexname * string) list -> - thm -> int -> tactic val set_tactic: (Proof.context -> thm list -> tactic) -> unit val tactic: string -> Proof.context -> method type src @@ -337,134 +335,6 @@ end; -(* rule_tac etc. -- refer to dynamic goal state!! *) (* FIXME cleanup!! *) - -fun bires_inst_tac bires_flag ctxt insts thm = - let - val thy = ProofContext.theory_of ctxt; - (* Separate type and term insts *) - fun has_type_var ((x, _), _) = (case Symbol.explode x of - "'"::cs => true | cs => false); - val Tinsts = List.filter has_type_var insts; - val tinsts = filter_out has_type_var insts; - (* Tactic *) - fun tac i st = - let - (* Preprocess state: extract environment information: - - variables and their types - - type variables and their sorts - - parameters and their types *) - val (types, sorts) = types_sorts st; - (* Process type insts: Tinsts_env *) - fun absent xi = error - ("No such variable in theorem: " ^ Syntax.string_of_vname xi); - val (rtypes, rsorts) = types_sorts thm; - fun readT (xi, s) = - let val S = case rsorts xi of SOME S => S | NONE => absent xi; - val T = Sign.read_typ (thy, sorts) s; - val U = TVar (xi, S); - in if Sign.typ_instance thy (T, U) then (U, T) - else error - ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails") - end; - val Tinsts_env = map readT Tinsts; - (* Preprocess rule: extract vars and their types, apply Tinsts *) - fun get_typ xi = - (case rtypes xi of - SOME T => typ_subst_atomic Tinsts_env T - | NONE => absent xi); - val (xis, ss) = Library.split_list tinsts; - val Ts = map get_typ xis; - val (_, _, Bi, _) = dest_state(st,i) - val params = Logic.strip_params Bi - (* params of subgoal i as string typ pairs *) - val params = rev(Term.rename_wrt_term Bi params) - (* as they are printed: bound variables with *) - (* the same name are renamed during printing *) - fun types' (a, ~1) = (case AList.lookup (op =) params a of - NONE => types (a, ~1) - | some => some) - | types' xi = types xi; - fun internal x = is_some (types' (x, ~1)); - val used = Drule.add_used thm (Drule.add_used st []); - val (ts, envT) = - ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts); - val envT' = map (fn (ixn, T) => - (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env; - val cenv = - map - (fn (xi, t) => - pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t)) - (distinct - (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) - (xis ~~ ts)); - (* Lift and instantiate rule *) - val {maxidx, ...} = rep_thm st; - val paramTs = map #2 params - and inc = maxidx+1 - fun liftvar (Var ((a,j), T)) = - Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T) - | liftvar t = raise TERM("Variable expected", [t]); - fun liftterm t = list_abs_free - (params, Logic.incr_indexes(paramTs,inc) t) - fun liftpair (cv,ct) = - (cterm_fun liftvar cv, cterm_fun liftterm ct) - val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc); - val rule = Drule.instantiate - (map lifttvar envT', map liftpair cenv) - (Thm.lift_rule (Thm.cprem_of st i) thm) - in - if i > nprems_of st then no_tac st - else st |> - compose_tac (bires_flag, rule, nprems_of thm) i - end - handle TERM (msg,_) => (warning msg; no_tac st) - | THM (msg,_,_) => (warning msg; no_tac st); - in tac end; - -local - -fun gen_inst _ tac _ (quant, ([], thms)) = - METHOD (fn facts => quant (insert_tac facts THEN' tac thms)) - | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) = - METHOD (fn facts => - quant (insert_tac facts THEN' inst_tac ctxt insts thm)) - | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules"; - -in - -val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac; - -val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac; - -val cut_inst_meth = - gen_inst - (fn ctxt => fn insts => bires_inst_tac false ctxt insts o Tactic.make_elim_preserve) - Tactic.cut_rules_tac; - -val dres_inst_meth = - gen_inst - (fn ctxt => fn insts => bires_inst_tac true ctxt insts o Tactic.make_elim_preserve) - Tactic.dresolve_tac; - -val forw_inst_meth = - gen_inst - (fn ctxt => fn insts => fn rule => - bires_inst_tac false ctxt insts (Tactic.make_elim_preserve rule) THEN' - assume_tac) - Tactic.forward_tac; - -fun subgoal_tac ctxt sprop = - DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl; - -fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops); - -fun thin_tac ctxt s = - bires_inst_tac true ctxt [(("V", 0), s)] thin_rl; - -end; - - (* ML tactics *) val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic); @@ -670,21 +540,6 @@ fun nat_thms_args f = uncurry f oo (#2 oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms)); -val insts = - Scan.optional - (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --| - Scan.lift (Args.$$$ "in")) [] -- Attrib.thms; - -fun inst_args f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts) src ctxt)); - -val insts_var = - Scan.optional - (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --| - Scan.lift (Args.$$$ "in")) [] -- Attrib.thms; - -fun inst_args_var f src ctxt = - f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt)); - fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >> (fn (quant, s) => SIMPLE_METHOD' quant (tac s))) src ctxt); @@ -697,14 +552,6 @@ fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac; -(* misc tactic emulations *) - -val subgoal_meth = goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac; -val thin_meth = goal_args_ctxt Args.name thin_tac; -val rename_meth = goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac; -val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac; - - (* theory setup *) val _ = Context.add_setup (add_methods @@ -726,15 +573,10 @@ ("this", no_args this, "apply current facts as rules"), ("fact", thms_ctxt_args fact, "composition by facts from context"), ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"), - ("rule_tac", inst_args_var res_inst_meth, "apply rule (dynamic instantiation)"), - ("erule_tac", inst_args_var eres_inst_meth, "apply rule in elimination manner (dynamic instantiation)"), - ("drule_tac", inst_args_var dres_inst_meth, "apply rule in destruct manner (dynamic instantiation)"), - ("frule_tac", inst_args_var forw_inst_meth, "apply rule in forward manner (dynamic instantiation)"), - ("cut_tac", inst_args_var cut_inst_meth, "cut rule (dynamic instantiation)"), - ("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation)"), - ("thin_tac", thin_meth, "remove premise (dynamic instantiation)"), - ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation)"), - ("rotate_tac", rotate_meth, "rotate assumptions of goal"), + ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac, + "rename parameters of goal (dynamic instantiation)"), + ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac, + "rotate assumptions of goal"), ("tactic", simple_args Args.name tactic, "ML tactic as proof method")]);