wenzelm@5824: (* Title: Pure/Isar/method.ML wenzelm@5824: ID: $Id$ wenzelm@5824: Author: Markus Wenzel, TU Muenchen wenzelm@5824: wenzelm@17110: Isar proof methods. wenzelm@5824: *) wenzelm@5824: wenzelm@5824: signature BASIC_METHOD = wenzelm@5824: sig wenzelm@17110: val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq wenzelm@17110: val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq wenzelm@17110: type method wenzelm@11731: val trace_rules: bool ref wenzelm@5824: val print_methods: theory -> unit wenzelm@17110: val Method: bstring -> (Args.src -> ProofContext.context -> method) -> string -> unit wenzelm@5824: end; wenzelm@5824: wenzelm@5824: signature METHOD = wenzelm@5824: sig wenzelm@5824: include BASIC_METHOD wenzelm@18227: val apply: method -> thm list -> cases_tactic wenzelm@18227: val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method wenzelm@17110: val RAW_METHOD: (thm list -> tactic) -> method wenzelm@18227: val METHOD_CASES: (thm list -> cases_tactic) -> method wenzelm@17110: val METHOD: (thm list -> tactic) -> method wenzelm@17110: val fail: method wenzelm@17110: val succeed: method wenzelm@17110: val insert_tac: thm list -> int -> tactic wenzelm@17110: val insert: thm list -> method wenzelm@17110: val insert_facts: method wenzelm@17110: val SIMPLE_METHOD: tactic -> method wenzelm@17110: val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> method wenzelm@17110: val defer: int option -> method wenzelm@17110: val prefer: int -> method wenzelm@17356: val cheating: bool -> ProofContext.context -> method wenzelm@17110: val intro: thm list -> method wenzelm@17110: val elim: thm list -> method wenzelm@17110: val unfold: thm list -> method wenzelm@17110: val fold: thm list -> method wenzelm@17110: val atomize: bool -> method wenzelm@17110: val this: method wenzelm@18039: val fact: thm list -> ProofContext.context -> method wenzelm@17110: val assumption: ProofContext.context -> method wenzelm@17110: val close: bool -> ProofContext.context -> method wenzelm@17110: val trace: ProofContext.context -> thm list -> unit wenzelm@6091: val rule_tac: thm list -> thm list -> int -> tactic wenzelm@17110: val some_rule_tac: thm list -> ProofContext.context -> thm list -> int -> tactic wenzelm@17110: val rule: thm list -> method wenzelm@17110: val erule: int -> thm list -> method wenzelm@17110: val drule: int -> thm list -> method wenzelm@17110: val frule: int -> thm list -> method nipkow@17587: val iprover_tac: ProofContext.context -> int option -> int -> tactic wenzelm@17110: val bires_inst_tac: bool -> ProofContext.context -> (indexname * string) list -> wenzelm@17110: thm -> int -> tactic wenzelm@17110: val set_tactic: (ProofContext.context -> thm list -> tactic) -> unit wenzelm@17110: val tactic: string -> ProofContext.context -> method wenzelm@17110: type src wenzelm@5824: datatype text = wenzelm@17110: Basic of (ProofContext.context -> method) | wenzelm@15703: Source of src | wenzelm@5824: Then of text list | wenzelm@5824: Orelse of text list | wenzelm@5824: Try of text | wenzelm@5824: Repeat1 of text wenzelm@17857: val primitive_text: (thm -> thm) -> text wenzelm@17857: val succeed_text: text wenzelm@17110: val default_text: text wenzelm@17110: val this_text: text wenzelm@17110: val done_text: text wenzelm@17356: val sorry_text: bool -> text wenzelm@17356: val finish_text: text option * bool -> text wenzelm@17110: exception METHOD_FAIL of (string * Position.T) * exn wenzelm@17110: val method: theory -> src -> ProofContext.context -> method wenzelm@17110: val add_methods: (bstring * (src -> ProofContext.context -> method) * string) list wenzelm@17110: -> theory -> theory wenzelm@17110: val add_method: bstring * (src -> ProofContext.context -> method) * string wenzelm@17110: -> theory -> theory wenzelm@17356: val method_setup: bstring * string * string -> theory -> theory wenzelm@17110: val syntax: (ProofContext.context * Args.T list -> 'a * (ProofContext.context * Args.T list)) wenzelm@17110: -> src -> ProofContext.context -> ProofContext.context * 'a wenzelm@17110: val simple_args: (Args.T list -> 'a * Args.T list) wenzelm@17110: -> ('a -> ProofContext.context -> method) -> src -> ProofContext.context -> method wenzelm@17110: val ctxt_args: (ProofContext.context -> method) -> src -> ProofContext.context -> method wenzelm@17110: val no_args: method -> src -> ProofContext.context -> method wenzelm@17110: type modifier wenzelm@17110: val sectioned_args: (ProofContext.context * Args.T list -> wenzelm@17110: 'a * (ProofContext.context * Args.T list)) -> wenzelm@17110: (Args.T list -> modifier * Args.T list) list -> wenzelm@17110: ('a -> ProofContext.context -> 'b) -> src -> ProofContext.context -> 'b wenzelm@17110: val bang_sectioned_args: wenzelm@17110: (Args.T list -> modifier * Args.T list) list -> wenzelm@17110: (thm list -> ProofContext.context -> 'a) -> src -> ProofContext.context -> 'a wenzelm@17110: val bang_sectioned_args': wenzelm@17110: (Args.T list -> modifier * Args.T list) list -> wenzelm@17110: (ProofContext.context * Args.T list -> 'a * (ProofContext.context * Args.T list)) -> wenzelm@17110: ('a -> thm list -> ProofContext.context -> 'b) -> src -> ProofContext.context -> 'b wenzelm@17110: val only_sectioned_args: wenzelm@17110: (Args.T list -> modifier * Args.T list) list -> wenzelm@17110: (ProofContext.context -> 'a) -> src -> ProofContext.context -> 'a wenzelm@17110: val thms_ctxt_args: (thm list -> ProofContext.context -> 'a) -> src -> wenzelm@17110: ProofContext.context -> 'a wenzelm@17110: val thms_args: (thm list -> 'a) -> src -> ProofContext.context -> 'a wenzelm@17110: val thm_args: (thm -> 'a) -> src -> ProofContext.context -> 'a wenzelm@9539: val goal_args: (Args.T list -> 'a * Args.T list) -> ('a -> int -> tactic) wenzelm@17110: -> src -> ProofContext.context -> method wenzelm@17110: val goal_args': (ProofContext.context * Args.T list -> wenzelm@17110: 'a * (ProofContext.context * Args.T list)) wenzelm@17110: -> ('a -> int -> tactic) -> src -> ProofContext.context -> method wenzelm@17110: val goal_args_ctxt: (Args.T list -> 'a * Args.T list) -> wenzelm@17110: (ProofContext.context -> 'a -> int -> tactic) -> src -> ProofContext.context -> method wenzelm@17110: val goal_args_ctxt': (ProofContext.context * Args.T list -> wenzelm@17110: 'a * (ProofContext.context * Args.T list)) -> wenzelm@17110: (ProofContext.context -> 'a -> int -> tactic) -> src -> ProofContext.context -> method wenzelm@5824: end; wenzelm@5824: wenzelm@5824: structure Method: METHOD = wenzelm@5824: struct wenzelm@5824: wenzelm@17110: (** generic tools **) wenzelm@17110: wenzelm@17110: (* goal addressing *) wenzelm@17110: wenzelm@17110: fun FINDGOAL tac st = wenzelm@17110: let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n) wenzelm@17110: in find 1 (Thm.nprems_of st) st end; wenzelm@17110: wenzelm@17110: fun HEADGOAL tac = tac 1; wenzelm@17110: wenzelm@17110: wenzelm@5824: wenzelm@12324: (** proof methods **) wenzelm@12324: wenzelm@17110: (* datatype method *) wenzelm@11731: wenzelm@18227: datatype method = Meth of thm list -> cases_tactic; wenzelm@11731: wenzelm@17756: fun apply (Meth m) = m; wenzelm@11731: wenzelm@17756: val RAW_METHOD_CASES = Meth; wenzelm@11731: wenzelm@17110: fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac); wenzelm@12144: wenzelm@17110: fun METHOD_CASES tac = RAW_METHOD_CASES (fn facts => wenzelm@17110: Seq.THEN (TRY Tactic.conjunction_tac, tac facts)); wenzelm@8372: wenzelm@17110: fun METHOD tac = RAW_METHOD (fn facts => wenzelm@17110: TRY Tactic.conjunction_tac THEN tac facts); wenzelm@5824: wenzelm@5824: val fail = METHOD (K no_tac); wenzelm@5824: val succeed = METHOD (K all_tac); wenzelm@5824: wenzelm@5824: wenzelm@17110: (* insert facts *) wenzelm@7419: wenzelm@7419: local wenzelm@5824: wenzelm@6981: fun cut_rule_tac raw_rule = wenzelm@6981: let wenzelm@6981: val rule = Drule.forall_intr_vars raw_rule; wenzelm@18039: val revcut_rl = Drule.incr_indexes rule Drule.revcut_rl; wenzelm@7555: in Tactic.rtac (rule COMP revcut_rl) end; wenzelm@6981: wenzelm@7419: in wenzelm@5824: wenzelm@7419: fun insert_tac [] i = all_tac wenzelm@7419: | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); wenzelm@6981: wenzelm@7555: val insert_facts = METHOD (ALLGOALS o insert_tac); wenzelm@7664: fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms)); wenzelm@7419: wenzelm@9706: fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac); wenzelm@9706: fun SIMPLE_METHOD' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac)); wenzelm@9706: wenzelm@12324: end; wenzelm@12324: wenzelm@9706: wenzelm@17110: (* shuffle subgoals *) wenzelm@17110: wenzelm@17110: fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1))); wenzelm@17110: fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1))); wenzelm@17110: wenzelm@17110: wenzelm@17356: (* cheating *) wenzelm@17356: wenzelm@17356: fun cheating int ctxt = METHOD (K (setmp quick_and_dirty (int orelse ! quick_and_dirty) wenzelm@17356: (SkipProof.cheat_tac (ProofContext.theory_of ctxt)))); wenzelm@17356: wenzelm@17356: wenzelm@17110: (* unfold intro/elim rules *) wenzelm@17110: wenzelm@17110: fun intro ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths)); wenzelm@17110: fun elim ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths)); wenzelm@17110: wenzelm@17110: wenzelm@12384: (* unfold/fold definitions *) wenzelm@12384: wenzelm@16145: fun unfold_meth ths = SIMPLE_METHOD (CHANGED_PROP (rewrite_goals_tac ths)); wenzelm@16145: fun fold_meth ths = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac ths)); wenzelm@6532: wenzelm@12384: wenzelm@12829: (* atomize rule statements *) wenzelm@12829: wenzelm@12829: fun atomize false = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac) wenzelm@12829: | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac))); wenzelm@12829: wenzelm@12829: wenzelm@18039: (* this -- resolve facts directly *) wenzelm@12384: wenzelm@17110: val this = METHOD (EVERY o map (HEADGOAL o Tactic.rtac)); wenzelm@9484: wenzelm@9484: wenzelm@18039: (* fact -- composition by facts from context *) wenzelm@18039: wenzelm@18309: fun fact [] ctxt = SIMPLE_METHOD' HEADGOAL (ProofContext.some_fact_tac ctxt) wenzelm@18309: | fact rules _ = SIMPLE_METHOD' HEADGOAL (ProofContext.fact_tac rules); wenzelm@18039: wenzelm@18039: wenzelm@17110: (* assumption *) wenzelm@7419: wenzelm@7419: local wenzelm@7419: wenzelm@17110: fun asm_tac ths = wenzelm@17110: foldr (op APPEND') (K no_tac) (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths); wenzelm@17110: wenzelm@17110: val refl_tac = SUBGOAL (fn (prop, i) => wenzelm@17110: if can Logic.dest_equals (Logic.strip_assums_concl prop) wenzelm@17110: then Tactic.rtac Drule.reflexive_thm i else no_tac); wenzelm@7419: wenzelm@17110: fun assm_tac ctxt = wenzelm@17110: assume_tac APPEND' wenzelm@17110: asm_tac (ProofContext.prems_of ctxt) APPEND' wenzelm@17110: refl_tac; wenzelm@17110: wenzelm@17110: fun assumption_tac ctxt [] = assm_tac ctxt wenzelm@17110: | assumption_tac _ [fact] = asm_tac [fact] wenzelm@17110: | assumption_tac _ _ = K no_tac; wenzelm@7419: wenzelm@7419: in wenzelm@7419: wenzelm@17110: fun assumption ctxt = METHOD (HEADGOAL o assumption_tac ctxt); wenzelm@17356: fun close immed ctxt = METHOD (K wenzelm@17356: (FILTER Thm.no_prems ((if immed then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac))); wenzelm@7419: wenzelm@7419: end; wenzelm@7419: wenzelm@7419: wenzelm@17110: (* rule etc. -- single-step refinements *) wenzelm@12347: wenzelm@17110: val trace_rules = ref false; wenzelm@12347: wenzelm@17110: fun trace ctxt rules = wenzelm@17110: conditional (! trace_rules andalso not (null rules)) (fn () => wenzelm@17110: Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules) wenzelm@17110: |> Pretty.string_of |> tracing); wenzelm@12347: wenzelm@12347: local wenzelm@12347: wenzelm@10541: fun gen_rule_tac tac rules [] i st = tac rules i st wenzelm@12324: | gen_rule_tac tac rules facts i st = wenzelm@18227: Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules); wenzelm@7130: wenzelm@10744: fun gen_arule_tac tac j rules facts = wenzelm@10744: EVERY' (gen_rule_tac tac rules facts :: replicate j Tactic.assume_tac); wenzelm@10744: wenzelm@11785: fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) => wenzelm@11785: let wenzelm@11785: val rules = wenzelm@11785: if not (null arg_rules) then arg_rules skalberg@15570: else List.concat (ContextRules.find_rules false facts goal ctxt) wenzelm@12055: in trace ctxt rules; tac rules facts i end); wenzelm@10309: wenzelm@10744: fun meth tac x = METHOD (HEADGOAL o tac x); wenzelm@10744: fun meth' tac x y = METHOD (HEADGOAL o tac x y); wenzelm@8220: wenzelm@7419: in wenzelm@7419: wenzelm@10744: val rule_tac = gen_rule_tac Tactic.resolve_tac; wenzelm@10744: val rule = meth rule_tac; wenzelm@10744: val some_rule_tac = gen_some_rule_tac rule_tac; wenzelm@10744: val some_rule = meth' some_rule_tac; wenzelm@10744: wenzelm@10744: val erule = meth' (gen_arule_tac Tactic.eresolve_tac); wenzelm@10744: val drule = meth' (gen_arule_tac Tactic.dresolve_tac); wenzelm@10744: val frule = meth' (gen_arule_tac Tactic.forward_tac); wenzelm@5824: wenzelm@7419: end; wenzelm@7419: wenzelm@7419: nipkow@17587: (* iprover -- intuitionistic proof search *) wenzelm@17110: wenzelm@17110: local wenzelm@17110: wenzelm@17110: val remdups_tac = SUBGOAL (fn (g, i) => wenzelm@17110: let val prems = Logic.strip_assums_hyp g in wenzelm@17110: REPEAT_DETERM_N (length prems - length (gen_distinct op aconv prems)) wenzelm@17110: (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i) wenzelm@17110: end); wenzelm@17110: wenzelm@17110: fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac; wenzelm@17110: wenzelm@17110: fun gen_eq_set e s1 s2 = wenzelm@17110: length s1 = length s2 andalso wenzelm@17110: gen_subset e (s1, s2) andalso gen_subset e (s2, s1); wenzelm@17110: wenzelm@17110: val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist; wenzelm@17110: wenzelm@17110: fun safe_step_tac ctxt = wenzelm@17110: ContextRules.Swrap ctxt wenzelm@17110: (eq_assume_tac ORELSE' wenzelm@17110: bires_tac true (ContextRules.netpair_bang ctxt)); wenzelm@8195: wenzelm@17110: fun unsafe_step_tac ctxt = wenzelm@17110: ContextRules.wrap ctxt wenzelm@17110: (assume_tac APPEND' wenzelm@17110: bires_tac false (ContextRules.netpair_bang ctxt) APPEND' wenzelm@17110: bires_tac false (ContextRules.netpair ctxt)); wenzelm@17110: wenzelm@17110: fun step_tac ctxt i = wenzelm@17110: REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE wenzelm@17110: REMDUPS (unsafe_step_tac ctxt) i; wenzelm@17110: wenzelm@17110: fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else wenzelm@17110: let wenzelm@17110: val ps = Logic.strip_assums_hyp g; wenzelm@17110: val c = Logic.strip_assums_concl g; wenzelm@17110: in wenzelm@17110: if gen_mem (fn ((ps1, c1), (ps2, c2)) => wenzelm@17110: c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) ((ps, c), gs) then no_tac wenzelm@17110: else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i wenzelm@17110: end); wenzelm@17110: wenzelm@17110: in wenzelm@17110: nipkow@17587: fun iprover_tac ctxt opt_lim = wenzelm@17110: SELECT_GOAL (DEEPEN (2, if_none opt_lim 20) (intprover_tac ctxt [] 0) 4 1); wenzelm@17110: wenzelm@17110: end; wenzelm@8195: wenzelm@8195: wenzelm@17110: (* rule_tac etc. -- refer to dynamic goal state!! *) wenzelm@12119: ballarin@14174: fun bires_inst_tac bires_flag ctxt insts thm = ballarin@14174: let wenzelm@17110: val thy = ProofContext.theory_of ctxt; ballarin@14174: (* Separate type and term insts *) ballarin@14174: fun has_type_var ((x, _), _) = (case Symbol.explode x of ballarin@14174: "'"::cs => true | cs => false); skalberg@15570: val Tinsts = List.filter has_type_var insts; ballarin@14174: val tinsts = filter_out has_type_var insts; ballarin@14174: (* Tactic *) ballarin@14174: fun tac i st = ballarin@14174: let ballarin@14174: (* Preprocess state: extract environment information: ballarin@14174: - variables and their types ballarin@14174: - type variables and their sorts ballarin@14174: - parameters and their types *) ballarin@14174: val (types, sorts) = types_sorts st; ballarin@14174: (* Process type insts: Tinsts_env *) ballarin@14174: fun absent xi = error wenzelm@14718: ("No such variable in theorem: " ^ Syntax.string_of_vname xi); ballarin@14174: val (rtypes, rsorts) = types_sorts thm; ballarin@14174: fun readT (xi, s) = skalberg@15531: let val S = case rsorts xi of SOME S => S | NONE => absent xi; wenzelm@17110: val T = Sign.read_typ (thy, sorts) s; berghofe@15798: val U = TVar (xi, S); wenzelm@17110: in if Sign.typ_instance thy (T, U) then (U, T) ballarin@14174: else error ballarin@14174: ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails") ballarin@14174: end; ballarin@14174: val Tinsts_env = map readT Tinsts; ballarin@14174: (* Preprocess rule: extract vars and their types, apply Tinsts *) ballarin@14174: fun get_typ xi = ballarin@14174: (case rtypes xi of berghofe@15798: SOME T => typ_subst_atomic Tinsts_env T skalberg@15531: | NONE => absent xi); ballarin@14174: val (xis, ss) = Library.split_list tinsts; ballarin@14174: val Ts = map get_typ xis; wenzelm@14718: val (_, _, Bi, _) = dest_state(st,i) wenzelm@14718: val params = Logic.strip_params Bi wenzelm@14718: (* params of subgoal i as string typ pairs *) wenzelm@14718: val params = rev(Term.rename_wrt_term Bi params) wenzelm@14718: (* as they are printed: bound variables with *) ballarin@14508: (* the same name are renamed during printing *) haftmann@17314: fun types' (a, ~1) = (case AList.lookup (op =) params a of skalberg@15531: NONE => types (a, ~1) ballarin@14174: | some => some) ballarin@14174: | types' xi = types xi; wenzelm@15973: fun internal x = is_some (types' (x, ~1)); wenzelm@15703: val used = Drule.add_used thm (Drule.add_used st []); wenzelm@14718: val (ts, envT) = wenzelm@14718: ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts); berghofe@15798: val envT' = map (fn (ixn, T) => wenzelm@15973: (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env; wenzelm@14718: val cenv = wenzelm@14718: map wenzelm@14718: (fn (xi, t) => wenzelm@17110: pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t)) wenzelm@14718: (gen_distinct wenzelm@14718: (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) wenzelm@14718: (xis ~~ ts)); wenzelm@14718: (* Lift and instantiate rule *) wenzelm@14718: val {maxidx, ...} = rep_thm st; wenzelm@14718: val paramTs = map #2 params wenzelm@14718: and inc = maxidx+1 wenzelm@14718: fun liftvar (Var ((a,j), T)) = wenzelm@16876: Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T) wenzelm@14718: | liftvar t = raise TERM("Variable expected", [t]); wenzelm@14718: fun liftterm t = list_abs_free wenzelm@14718: (params, Logic.incr_indexes(paramTs,inc) t) wenzelm@14718: fun liftpair (cv,ct) = wenzelm@14718: (cterm_fun liftvar cv, cterm_fun liftterm ct) wenzelm@17110: val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc); wenzelm@14718: val rule = Drule.instantiate berghofe@15798: (map lifttvar envT', map liftpair cenv) wenzelm@18145: (Thm.lift_rule (Thm.cprem_of st i) thm) ballarin@14174: in wenzelm@14718: if i > nprems_of st then no_tac st wenzelm@14718: else st |> wenzelm@14718: compose_tac (bires_flag, rule, nprems_of thm) i ballarin@14174: end wenzelm@14718: handle TERM (msg,_) => (warning msg; no_tac st) wenzelm@14718: | THM (msg,_,_) => (warning msg; no_tac st); ballarin@14174: in ballarin@14174: tac ballarin@14174: end; wenzelm@8238: wenzelm@17110: local wenzelm@17110: ballarin@14174: fun gen_inst _ tac _ (quant, ([], thms)) = ballarin@14174: METHOD (fn facts => quant (insert_tac facts THEN' tac thms)) ballarin@14174: | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) = ballarin@14174: METHOD (fn facts => ballarin@14174: quant (insert_tac facts THEN' inst_tac ctxt insts thm)) ballarin@14174: | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules"; wenzelm@14718: ballarin@14174: (* Preserve Var indexes of rl; increment revcut_rl instead. ballarin@14174: Copied from tactic.ML *) ballarin@14174: fun make_elim_preserve rl = ballarin@14174: let val {maxidx,...} = rep_thm rl wenzelm@17110: fun cvar xi = cterm_of ProtoPure.thy (Var(xi,propT)); ballarin@14174: val revcut_rl' = ballarin@14174: instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), ballarin@14174: (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl ballarin@14174: val arg = (false, rl, nprems_of rl) ballarin@14174: val [th] = Seq.list_of (bicompose false arg 1 revcut_rl') ballarin@14174: in th end ballarin@14174: handle Bind => raise THM("make_elim_preserve", 1, [rl]); wenzelm@8238: wenzelm@17110: in wenzelm@17110: wenzelm@17110: val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac; wenzelm@17110: wenzelm@17110: val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac; wenzelm@17110: ballarin@14174: val cut_inst_meth = ballarin@14174: gen_inst wenzelm@17110: (fn ctxt => fn insts => bires_inst_tac false ctxt insts o make_elim_preserve) ballarin@14174: Tactic.cut_rules_tac; ballarin@14174: ballarin@14174: val dres_inst_meth = ballarin@14174: gen_inst wenzelm@17110: (fn ctxt => fn insts => bires_inst_tac true ctxt insts o make_elim_preserve) ballarin@14174: Tactic.dresolve_tac; ballarin@14174: ballarin@14174: val forw_inst_meth = ballarin@14174: gen_inst ballarin@14174: (fn ctxt => fn insts => fn rule => ballarin@14174: bires_inst_tac false ctxt insts (make_elim_preserve rule) THEN' ballarin@14174: assume_tac) ballarin@14174: Tactic.forward_tac; ballarin@14174: ballarin@14174: fun subgoal_tac ctxt sprop = wenzelm@17110: DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl; ballarin@14174: ballarin@14174: fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops); ballarin@14174: ballarin@14174: fun thin_tac ctxt s = ballarin@14174: bires_inst_tac true ctxt [(("V", 0), s)] thin_rl; wenzelm@8238: wenzelm@17110: end; wenzelm@8329: wenzelm@8329: wenzelm@8351: (* ML tactics *) wenzelm@8351: wenzelm@17110: val tactic_ref = ref ((fn _ => raise Match): ProofContext.context -> thm list -> tactic); wenzelm@8351: fun set_tactic f = tactic_ref := f; wenzelm@8351: wenzelm@8351: fun tactic txt ctxt = METHOD (fn facts => wenzelm@9631: (Context.use_mltext wenzelm@17110: ("let fun tactic (ctxt: ProofContext.context) (facts: thm list) : tactic = \ wenzelm@16500: \let val thm = ProofContext.get_thm_closure ctxt o PureThy.Name\n\ wenzelm@16500: \ and thms = ProofContext.get_thms_closure ctxt o PureThy.Name in\n" wenzelm@16500: ^ txt ^ wenzelm@16500: "\nend in Method.set_tactic tactic end") skalberg@15531: false NONE; skalberg@15531: Context.setmp (SOME (ProofContext.theory_of ctxt)) (! tactic_ref ctxt) facts)); wenzelm@8351: wenzelm@8351: wenzelm@5824: wenzelm@17110: (** method syntax **) wenzelm@17110: wenzelm@17110: (* method text *) wenzelm@17110: wenzelm@17110: type src = Args.src; wenzelm@5824: wenzelm@17110: datatype text = wenzelm@17110: Basic of (ProofContext.context -> method) | wenzelm@17110: Source of src | wenzelm@17110: Then of text list | wenzelm@17110: Orelse of text list | wenzelm@17110: Try of text | wenzelm@17110: Repeat1 of text; wenzelm@17110: wenzelm@17857: val primitive_text = Basic o K o SIMPLE_METHOD o PRIMITIVE; wenzelm@17857: val succeed_text = Basic (K succeed); wenzelm@17110: val default_text = Source (Args.src (("default", []), Position.none)); wenzelm@17110: val this_text = Basic (K this); wenzelm@17110: val done_text = Basic (K (SIMPLE_METHOD all_tac)); wenzelm@17356: val sorry_text = Basic o cheating; wenzelm@17110: wenzelm@17356: fun finish_text (NONE, immed) = Basic (close immed) wenzelm@17356: | finish_text (SOME txt, immed) = Then [txt, Basic (close immed)]; wenzelm@17110: wenzelm@17110: wenzelm@17110: (* method definitions *) wenzelm@5824: wenzelm@16448: structure MethodsData = TheoryDataFun wenzelm@16448: (struct wenzelm@5824: val name = "Isar/methods"; wenzelm@17110: type T = (((src -> ProofContext.context -> method) * string) * stamp) NameSpace.table; wenzelm@5824: wenzelm@16347: val empty = NameSpace.empty_table; wenzelm@6546: val copy = I; wenzelm@16448: val extend = I; haftmann@17496: fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups => wenzelm@16347: error ("Attempt to merge different versions of method(s) " ^ commas_quote dups); wenzelm@5824: wenzelm@16347: fun print _ meths = wenzelm@5824: let wenzelm@5824: fun prt_meth (name, ((_, comment), _)) = Pretty.block wenzelm@6849: [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; wenzelm@5824: in wenzelm@16347: [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))] wenzelm@9222: |> Pretty.chunks |> Pretty.writeln wenzelm@5824: end; wenzelm@16448: end); wenzelm@5824: wenzelm@15801: val _ = Context.add_setup [MethodsData.init]; wenzelm@5824: val print_methods = MethodsData.print; wenzelm@7611: wenzelm@5824: wenzelm@5824: (* get methods *) wenzelm@5824: wenzelm@5916: exception METHOD_FAIL of (string * Position.T) * exn; wenzelm@5916: wenzelm@5824: fun method thy = wenzelm@5824: let wenzelm@16347: val (space, meths) = MethodsData.get thy; wenzelm@5884: fun meth src = wenzelm@5884: let wenzelm@5884: val ((raw_name, _), pos) = Args.dest_src src; wenzelm@5884: val name = NameSpace.intern space raw_name; wenzelm@5884: in wenzelm@17412: (case Symtab.lookup meths name of skalberg@15531: NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos) skalberg@15531: | SOME ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src)) wenzelm@5824: end; wenzelm@5824: in meth end; wenzelm@5824: wenzelm@5824: wenzelm@17110: (* add method *) wenzelm@5824: wenzelm@5824: fun add_methods raw_meths thy = wenzelm@5824: let wenzelm@16145: val new_meths = raw_meths |> map (fn (name, f, comment) => wenzelm@16347: (name, ((f, comment), stamp ()))); wenzelm@5824: wenzelm@17110: fun add meths = NameSpace.extend_table (Sign.naming_of thy) (meths, new_meths) wenzelm@16347: handle Symtab.DUPS dups => wenzelm@16347: error ("Duplicate declaration of method(s) " ^ commas_quote dups); wenzelm@16347: in MethodsData.map add thy end; wenzelm@5824: wenzelm@9194: val add_method = add_methods o Library.single; wenzelm@9194: wenzelm@5824: fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]); wenzelm@5824: wenzelm@5824: wenzelm@17356: (* method_setup *) wenzelm@17356: wenzelm@17356: fun method_setup (name, txt, cmt) = wenzelm@17356: Context.use_let wenzelm@17356: "val thm = PureThy.get_thm_closure (Context.the_context ()) o PureThy.Name;\n\ wenzelm@17356: \val thms = PureThy.get_thms_closure (Context.the_context ()) o PureThy.Name;\n\ wenzelm@17356: \val method: bstring * (Method.src -> ProofContext.context -> Proof.method) * string" wenzelm@17356: "Method.add_method method" wenzelm@17356: ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")"); wenzelm@17356: wenzelm@17356: wenzelm@5884: wenzelm@17110: (** concrete syntax **) wenzelm@5824: wenzelm@5884: (* basic *) wenzelm@5884: wenzelm@17110: fun syntax (scan: wenzelm@17110: (ProofContext.context * Args.T list -> 'a * (ProofContext.context * Args.T list))) = wenzelm@5884: Args.syntax "method" scan; wenzelm@5824: wenzelm@17110: fun simple_args scan f src ctxt : method = wenzelm@8351: #2 (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt); wenzelm@8351: wenzelm@17110: fun ctxt_args (f: ProofContext.context -> method) src ctxt = wenzelm@8282: #2 (syntax (Scan.succeed (f ctxt)) src ctxt); wenzelm@7555: wenzelm@7555: fun no_args m = ctxt_args (K m); wenzelm@5884: wenzelm@5884: wenzelm@5884: (* sections *) wenzelm@5824: wenzelm@17110: type modifier = (ProofContext.context -> ProofContext.context) * ProofContext.context attribute; wenzelm@7268: wenzelm@7268: local wenzelm@7268: wenzelm@8381: fun sect ss = Scan.first (map Scan.lift ss); wenzelm@5884: fun thms ss = Scan.unless (sect ss) Attrib.local_thms; skalberg@15570: fun thmss ss = Scan.repeat (thms ss) >> List.concat; wenzelm@5884: wenzelm@7268: fun apply (f, att) (ctxt, ths) = Thm.applys_attributes ((f ctxt, ths), [att]); wenzelm@5824: wenzelm@7268: fun section ss = (sect ss -- thmss ss) :-- (fn (m, ths) => Scan.depend (fn ctxt => wenzelm@7268: Scan.succeed (apply m (ctxt, ths)))) >> #2; wenzelm@5884: wenzelm@7601: fun sectioned args ss = args -- Scan.repeat (section ss); wenzelm@5884: wenzelm@7268: in wenzelm@5824: wenzelm@5884: fun sectioned_args args ss f src ctxt = wenzelm@8282: let val (ctxt', (x, _)) = syntax (sectioned args ss) src ctxt wenzelm@5921: in f x ctxt' end; wenzelm@5884: wenzelm@7601: fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f; wenzelm@9777: fun bang_sectioned_args' ss scan f = wenzelm@9777: sectioned_args (Args.bang_facts -- scan >> swap) ss (uncurry f); wenzelm@7601: fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f); wenzelm@7268: wenzelm@8093: fun thms_ctxt_args f = sectioned_args (thmss []) [] f; wenzelm@8093: fun thms_args f = thms_ctxt_args (K o f); wenzelm@9706: fun thm_args f = thms_args (fn [thm] => f thm | _ => error "Single theorem expected"); wenzelm@5824: wenzelm@7268: end; wenzelm@7268: wenzelm@5824: nipkow@17587: (* iprover syntax *) wenzelm@12347: wenzelm@12347: local wenzelm@12347: wenzelm@12347: val introN = "intro"; wenzelm@12347: val elimN = "elim"; wenzelm@12347: val destN = "dest"; wenzelm@12347: val ruleN = "rule"; wenzelm@12347: wenzelm@12347: fun modifier name kind kind' att = skalberg@15531: Args.$$$ name |-- (kind >> K NONE || kind' |-- Args.nat --| Args.colon >> SOME) wenzelm@17110: >> (pair (I: ProofContext.context -> ProofContext.context) o att); wenzelm@12347: nipkow@17587: val iprover_modifiers = wenzelm@12384: [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang_local, wenzelm@12350: modifier destN Args.colon (Scan.succeed ()) ContextRules.dest_local, wenzelm@12350: modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang_local, wenzelm@12350: modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim_local, wenzelm@12350: modifier introN Args.bang_colon Args.bang ContextRules.intro_bang_local, wenzelm@12350: modifier introN Args.colon (Scan.succeed ()) ContextRules.intro_local, wenzelm@12350: Args.del -- Args.colon >> K (I, ContextRules.rule_del_local)]; wenzelm@12347: wenzelm@12347: in wenzelm@12347: nipkow@17587: fun iprover_args m = bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option Args.nat)) m; wenzelm@12347: nipkow@17587: fun iprover_meth n prems ctxt = METHOD (fn facts => nipkow@17587: HEADGOAL (insert_tac (prems @ facts) THEN' ObjectLogic.atomize_tac THEN' iprover_tac ctxt n)); wenzelm@12347: wenzelm@12347: end; wenzelm@12347: wenzelm@12347: wenzelm@9539: (* tactic syntax *) wenzelm@8238: wenzelm@10744: fun nat_thms_args f = uncurry f oo wenzelm@10744: (#2 oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.local_thmss)); wenzelm@10744: wenzelm@8238: val insts = wenzelm@9539: Scan.optional wenzelm@9565: (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --| wenzelm@9565: Scan.lift (Args.$$$ "in")) [] -- Attrib.local_thmss; wenzelm@8238: wenzelm@12119: fun inst_args f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts) src ctxt)); wenzelm@8537: ballarin@14174: val insts_var = ballarin@14174: Scan.optional ballarin@14174: (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --| ballarin@14174: Scan.lift (Args.$$$ "in")) [] -- Attrib.local_thmss; ballarin@14174: wenzelm@17110: fun inst_args_var f src ctxt = wenzelm@17110: f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt)); wenzelm@8537: wenzelm@12119: fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >> ballarin@14215: (fn (quant, s) => SIMPLE_METHOD' quant (tac s))) src ctxt); wenzelm@8537: wenzelm@9539: fun goal_args args tac = goal_args' (Scan.lift args) tac; wenzelm@8238: ballarin@14174: fun goal_args_ctxt' args tac src ctxt = ballarin@14174: #2 (syntax (Args.goal_spec HEADGOAL -- args >> ballarin@14174: (fn (quant, s) => SIMPLE_METHOD' quant (tac ctxt s))) src ctxt); wenzelm@8238: ballarin@14174: fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac; wenzelm@5824: wenzelm@14718: wenzelm@9539: (* misc tactic emulations *) wenzelm@9539: ballarin@14174: val subgoal_meth = goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac; ballarin@14174: val thin_meth = goal_args_ctxt Args.name thin_tac; wenzelm@9539: val rename_meth = goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac; wenzelm@9631: val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac; wenzelm@9539: wenzelm@9539: wenzelm@5824: (* pure_methods *) wenzelm@5824: wenzelm@5824: val pure_methods = wenzelm@5824: [("fail", no_args fail, "force failure"), wenzelm@5824: ("succeed", no_args succeed, "succeed"), wenzelm@9587: ("-", no_args insert_facts, "do nothing (insert current facts only)"), wenzelm@9539: ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"), wenzelm@16145: ("unfold", thms_args unfold_meth, "unfold definitions"), wenzelm@12384: ("intro", thms_args intro, "repeatedly apply introduction rules"), wenzelm@12384: ("elim", thms_args elim, "repeatedly apply elimination rules"), wenzelm@16145: ("fold", thms_args fold_meth, "fold definitions"), wenzelm@12829: ("atomize", (atomize o #2) oo syntax (Args.mode "full"), wenzelm@11962: "present local premises as object-level statements"), nipkow@17587: ("iprover", iprover_args iprover_meth, "intuitionistic proof search"), wenzelm@12384: ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"), wenzelm@10744: ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"), wenzelm@10744: ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"), wenzelm@10744: ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"), wenzelm@8195: ("this", no_args this, "apply current facts as rules"), wenzelm@18039: ("fact", thms_ctxt_args fact, "composition by facts from context"), wenzelm@8238: ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"), ballarin@14174: ("rule_tac", inst_args_var res_inst_meth, "apply rule (dynamic instantiation)"), ballarin@14174: ("erule_tac", inst_args_var eres_inst_meth, "apply rule in elimination manner (dynamic instantiation)"), ballarin@14174: ("drule_tac", inst_args_var dres_inst_meth, "apply rule in destruct manner (dynamic instantiation)"), ballarin@14174: ("frule_tac", inst_args_var forw_inst_meth, "apply rule in forward manner (dynamic instantiation)"), ballarin@14174: ("cut_tac", inst_args_var cut_inst_meth, "cut rule (dynamic instantiation)"), ballarin@14174: ("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation)"), ballarin@14174: ("thin_tac", thin_meth, "remove premise (dynamic instantiation)"), ballarin@14174: ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation)"), wenzelm@9631: ("rotate_tac", rotate_meth, "rotate assumptions of goal"), wenzelm@8351: ("tactic", simple_args Args.name tactic, "ML tactic as proof method")]; wenzelm@5824: wenzelm@15801: val _ = Context.add_setup [add_methods pure_methods]; wenzelm@5824: wenzelm@5824: wenzelm@16145: (*final declarations of this structure!*) wenzelm@16145: val unfold = unfold_meth; wenzelm@16145: val fold = fold_meth; wenzelm@16145: wenzelm@5824: end; wenzelm@5824: wenzelm@5824: structure BasicMethod: BASIC_METHOD = Method; wenzelm@5824: open BasicMethod;