wenzelm@5824: (* Title: Pure/Isar/method.ML wenzelm@5824: ID: $Id$ wenzelm@5824: Author: Markus Wenzel, TU Muenchen wenzelm@5824: wenzelm@5824: Proof methods. wenzelm@5824: *) wenzelm@5824: wenzelm@5824: signature BASIC_METHOD = wenzelm@5824: sig wenzelm@5824: val print_methods: theory -> unit wenzelm@5824: val Method: bstring -> (Args.src -> Proof.context -> Proof.method) -> string -> unit wenzelm@5824: end; wenzelm@5824: wenzelm@5824: signature METHOD = wenzelm@5824: sig wenzelm@5824: include BASIC_METHOD wenzelm@6500: val FINISHED: tactic -> tactic wenzelm@6091: val LIFT: tactic -> thm -> (thm * (indexname * term) list * (string * thm list) list) Seq.seq wenzelm@6091: val METHOD: (thm list -> tactic) -> Proof.method wenzelm@5824: val METHOD0: tactic -> Proof.method wenzelm@5824: val fail: Proof.method wenzelm@5824: val succeed: Proof.method wenzelm@6500: val same_tac: thm list -> int -> tactic wenzelm@6108: val same: Proof.method wenzelm@5824: val assumption: Proof.method wenzelm@5824: val forward_chain: thm list -> thm list -> thm Seq.seq wenzelm@6091: val rule_tac: thm list -> thm list -> int -> tactic wenzelm@6091: val rule: thm list -> Proof.method wenzelm@5916: exception METHOD_FAIL of (string * Position.T) * exn wenzelm@5824: val method: theory -> Args.src -> Proof.context -> Proof.method wenzelm@5824: val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list wenzelm@5824: -> theory -> theory wenzelm@5884: val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) -> wenzelm@5884: Proof.context -> Args.src -> Proof.context * 'a wenzelm@5884: val no_args: Proof.method -> Args.src -> Proof.context -> Proof.method wenzelm@5884: val sectioned_args: ((Args.T list -> Proof.context attribute * Args.T list) list -> wenzelm@5884: Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) -> wenzelm@5884: (Args.T list -> Proof.context attribute * Args.T list) list -> wenzelm@5884: ('a -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method wenzelm@5884: val default_sectioned_args: Proof.context attribute -> wenzelm@5884: (Args.T list -> Proof.context attribute * Args.T list) list -> wenzelm@5884: (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method wenzelm@5884: val only_sectioned_args: (Args.T list -> Proof.context attribute * Args.T list) list -> wenzelm@5884: (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method wenzelm@6091: val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method wenzelm@5824: datatype text = wenzelm@5824: Basic of (Proof.context -> Proof.method) | wenzelm@5824: Source of Args.src | wenzelm@5824: Then of text list | wenzelm@5824: Orelse of text list | wenzelm@5824: Try of text | wenzelm@5824: Repeat of text | wenzelm@5824: Repeat1 of text wenzelm@5824: val refine: text -> Proof.state -> Proof.state Seq.seq wenzelm@5824: val tac: text -> Proof.state -> Proof.state Seq.seq wenzelm@5884: val then_tac: text -> Proof.state -> Proof.state Seq.seq wenzelm@5824: val proof: text option -> Proof.state -> Proof.state Seq.seq wenzelm@6404: val local_qed: text option -> Proof.state -> Proof.state Seq.seq wenzelm@6404: val local_terminal_proof: text -> Proof.state -> Proof.state Seq.seq wenzelm@6404: val local_immediate_proof: Proof.state -> Proof.state Seq.seq wenzelm@6404: val local_default_proof: Proof.state -> Proof.state Seq.seq wenzelm@6404: val global_qed: bstring option -> theory attribute list option -> text option wenzelm@6532: -> Proof.state -> theory * {kind: string, name: string, thm: thm} wenzelm@6532: val global_terminal_proof: text -> Proof.state -> theory * {kind: string, name: string, thm: thm} wenzelm@6532: val global_immediate_proof: Proof.state -> theory * {kind: string, name: string, thm: thm} wenzelm@6532: val global_default_proof: Proof.state -> theory * {kind: string, name: string, thm: thm} wenzelm@5824: val setup: (theory -> theory) list wenzelm@5824: end; wenzelm@5824: wenzelm@5824: structure Method: METHOD = wenzelm@5824: struct wenzelm@5824: wenzelm@5824: wenzelm@6500: (** utils **) wenzelm@6500: wenzelm@6500: val FINISHED = FILTER (equal 0 o Thm.nprems_of); wenzelm@6500: wenzelm@6500: wenzelm@6500: wenzelm@5824: (** proof methods **) wenzelm@5824: wenzelm@5824: (* method from tactic *) wenzelm@5824: wenzelm@5824: fun LIFT tac goal = Seq.map (fn x => (x, [], [])) (tac goal); wenzelm@5824: fun METHOD tacf = Proof.method (LIFT o tacf); wenzelm@5824: fun METHOD0 tac = METHOD (fn [] => tac | _ => error "Method may not be used with facts"); wenzelm@5824: wenzelm@5824: wenzelm@5824: (* primitive *) wenzelm@5824: wenzelm@5824: val fail = METHOD (K no_tac); wenzelm@5824: val succeed = METHOD (K all_tac); wenzelm@5824: wenzelm@5824: wenzelm@6108: (* same, assumption *) wenzelm@5824: wenzelm@6108: fun same_tac [] = K all_tac wenzelm@6108: | same_tac facts = wenzelm@6091: let val r = ~ (length facts); wenzelm@6091: in metacuts_tac facts THEN' rotate_tac r end; wenzelm@5824: wenzelm@6108: val same = METHOD (ALLGOALS o same_tac); wenzelm@6108: val assumption = METHOD (fn facts => FIRSTGOAL (same_tac facts THEN' assume_tac)); wenzelm@5824: wenzelm@6500: val asm_finish = METHOD (K (FINISHED (ALLGOALS assume_tac))); wenzelm@5824: wenzelm@5824: wenzelm@6532: (* fold / unfold definitions *) wenzelm@6532: wenzelm@6532: val fold = METHOD0 o fold_goals_tac; wenzelm@6532: val unfold = METHOD0 o rewrite_goals_tac; wenzelm@6532: wenzelm@6532: wenzelm@5824: (* rule *) wenzelm@5824: wenzelm@5824: fun res th i rule = Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty; wenzelm@5824: wenzelm@5824: fun multi_resolve facts rule = wenzelm@5824: let wenzelm@5824: fun multi_res i [] = Seq.single rule wenzelm@5824: | multi_res i (th :: ths) = Seq.flat (Seq.map (res th i) (multi_res (i + 1) ths)) wenzelm@5824: in multi_res 1 facts end; wenzelm@5824: wenzelm@5824: fun forward_chain facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules)); wenzelm@5824: wenzelm@6091: fun rule_tac rules [] = resolve_tac rules wenzelm@5824: | rule_tac erules facts = wenzelm@5824: let wenzelm@6091: val rules = forward_chain facts erules; wenzelm@5824: fun tac i state = Seq.flat (Seq.map (fn rule => Tactic.rtac rule i state) rules); wenzelm@5824: in tac end; wenzelm@5824: wenzelm@5824: fun rule rules = METHOD (FIRSTGOAL o rule_tac rules); wenzelm@5824: wenzelm@5824: wenzelm@5824: wenzelm@5824: (** methods theory data **) wenzelm@5824: wenzelm@5824: (* data kind 'Isar/methods' *) wenzelm@5824: wenzelm@5824: structure MethodsDataArgs = wenzelm@5824: struct wenzelm@5824: val name = "Isar/methods"; wenzelm@5824: type T = wenzelm@5824: {space: NameSpace.T, wenzelm@5824: meths: (((Args.src -> Proof.context -> Proof.method) * string) * stamp) Symtab.table}; wenzelm@5824: wenzelm@5824: val empty = {space = NameSpace.empty, meths = Symtab.empty}; wenzelm@5824: val prep_ext = I; wenzelm@5824: fun merge ({space = space1, meths = meths1}, {space = space2, meths = meths2}) = wenzelm@5824: {space = NameSpace.merge (space1, space2), wenzelm@5824: meths = Symtab.merge eq_snd (meths1, meths2) handle Symtab.DUPS dups => wenzelm@5824: error ("Attempt to merge different versions of methods " ^ commas_quote dups)}; wenzelm@5824: wenzelm@5824: fun print _ {space, meths} = wenzelm@5824: let wenzelm@5824: fun prt_meth (name, ((_, comment), _)) = Pretty.block wenzelm@5824: [Pretty.str (NameSpace.cond_extern space name ^ ":"), Pretty.brk 2, Pretty.str comment]; wenzelm@5824: in wenzelm@5824: Pretty.writeln (Display.pretty_name_space ("method name space", space)); wenzelm@5824: Pretty.writeln (Pretty.big_list "methods:" (map prt_meth (Symtab.dest meths))) wenzelm@5824: end; wenzelm@5824: end; wenzelm@5824: wenzelm@5824: structure MethodsData = TheoryDataFun(MethodsDataArgs); wenzelm@5824: val print_methods = MethodsData.print; wenzelm@5824: 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@5824: val {space, meths} = MethodsData.get thy; wenzelm@5824: 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@5824: (case Symtab.lookup (meths, name) of wenzelm@5824: None => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos) wenzelm@5916: | Some ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src)) wenzelm@5824: end; wenzelm@5824: in meth end; wenzelm@5824: wenzelm@5824: wenzelm@5824: (* add_methods *) wenzelm@5824: wenzelm@5824: fun add_methods raw_meths thy = wenzelm@5824: let wenzelm@5824: val full = Sign.full_name (Theory.sign_of thy); wenzelm@5824: val new_meths = wenzelm@5824: map (fn (name, f, comment) => (full name, ((f, comment), stamp ()))) raw_meths; wenzelm@5824: wenzelm@5824: val {space, meths} = MethodsData.get thy; wenzelm@5824: val space' = NameSpace.extend (space, map fst new_meths); wenzelm@5824: val meths' = Symtab.extend (meths, new_meths) handle Symtab.DUPS dups => wenzelm@5824: error ("Duplicate declaration of method(s) " ^ commas_quote dups); wenzelm@5824: in wenzelm@5824: thy |> MethodsData.put {space = space', meths = meths'} wenzelm@5824: end; wenzelm@5824: wenzelm@5824: (*implicit version*) wenzelm@5824: fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]); wenzelm@5824: wenzelm@5824: wenzelm@5884: wenzelm@5884: (** method syntax **) wenzelm@5824: wenzelm@5884: (* basic *) wenzelm@5884: wenzelm@5884: fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) = wenzelm@5884: Args.syntax "method" scan; wenzelm@5824: wenzelm@5884: fun no_args (x: Proof.method) src ctxt = #2 (syntax (Scan.succeed x) ctxt src); wenzelm@5884: wenzelm@5884: wenzelm@5884: (* sections *) wenzelm@5824: wenzelm@5884: fun sect ss = Scan.first (map (fn s => Scan.lift (s --| Args.$$$ ":")) ss); wenzelm@5884: fun thms ss = Scan.unless (sect ss) Attrib.local_thms; wenzelm@5884: fun thmss ss = Scan.repeat (thms ss) >> flat; wenzelm@5884: wenzelm@6091: fun apply att (ctxt, ths) = Thm.applys_attributes ((ctxt, ths), [att]); wenzelm@5824: wenzelm@5884: fun section ss = (sect ss -- thmss ss) :-- (fn (att, ths) => Scan.depend (fn ctxt => wenzelm@5884: Scan.succeed (apply att (ctxt, ths)))) >> #2; wenzelm@5884: wenzelm@5884: fun sectioned args ss = args ss -- Scan.repeat (section ss); wenzelm@5884: wenzelm@5824: wenzelm@5884: fun sectioned_args args ss f src ctxt = wenzelm@5921: let val (ctxt', (x, _)) = syntax (sectioned args ss) ctxt src wenzelm@5921: in f x ctxt' end; wenzelm@5884: wenzelm@5884: fun default_sectioned_args att ss f src ctxt = wenzelm@5884: sectioned_args thmss ss (fn ths => fn ctxt' => f (#1 (apply att (ctxt', ths)))) src ctxt; wenzelm@5884: wenzelm@5884: fun only_sectioned_args ss f = sectioned_args (K (Scan.succeed ())) ss (fn () => f); wenzelm@5884: fun thms_args f = sectioned_args thmss [] (fn ths => fn _ => f ths); wenzelm@5824: wenzelm@5824: wenzelm@5824: wenzelm@5824: (** method text **) wenzelm@5824: wenzelm@5824: (* datatype text *) wenzelm@5824: wenzelm@5824: datatype text = wenzelm@5824: Basic of (Proof.context -> Proof.method) | wenzelm@5824: Source of Args.src | wenzelm@5824: Then of text list | wenzelm@5824: Orelse of text list | wenzelm@5824: Try of text | wenzelm@5824: Repeat of text | wenzelm@5824: Repeat1 of text; wenzelm@5824: wenzelm@5824: wenzelm@5824: (* refine *) wenzelm@5824: wenzelm@5824: fun refine text state = wenzelm@5824: let wenzelm@5824: val thy = Proof.theory_of state; wenzelm@5824: wenzelm@5824: fun eval (Basic mth) = Proof.refine mth wenzelm@5824: | eval (Source src) = Proof.refine (method thy src) wenzelm@5824: | eval (Then txts) = Seq.EVERY (map eval txts) wenzelm@5824: | eval (Orelse txts) = Seq.FIRST (map eval txts) wenzelm@5824: | eval (Try txt) = Seq.TRY (eval txt) wenzelm@5824: | eval (Repeat txt) = Seq.REPEAT (eval txt) wenzelm@5824: | eval (Repeat1 txt) = Seq.REPEAT1 (eval txt); wenzelm@5824: in eval text state end; wenzelm@5824: wenzelm@6404: fun named_method name = Source (Args.src ((name, []), Position.none)); wenzelm@6404: wenzelm@5824: wenzelm@5824: (* unstructured steps *) wenzelm@5824: wenzelm@5824: fun tac text state = wenzelm@5824: state wenzelm@5824: |> Proof.goal_facts (K []) wenzelm@5824: |> refine text; wenzelm@5824: wenzelm@5884: fun then_tac text state = wenzelm@5824: state wenzelm@5824: |> Proof.goal_facts Proof.the_facts wenzelm@5824: |> refine text; wenzelm@5824: wenzelm@5824: wenzelm@6404: (* structured proof steps *) wenzelm@5824: wenzelm@6404: val default_text = named_method "default"; wenzelm@6404: val finish_text = named_method "finish"; wenzelm@5824: wenzelm@5824: fun proof opt_text state = wenzelm@5824: state wenzelm@5824: |> Proof.assert_backward wenzelm@6404: |> refine (if_none opt_text default_text) wenzelm@5824: |> Seq.map Proof.enter_forward; wenzelm@5824: wenzelm@6404: fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text)); wenzelm@6404: fun local_terminal_proof text = Seq.THEN (proof (Some text), local_qed None); wenzelm@6404: val local_immediate_proof = local_terminal_proof (Basic (K same)); wenzelm@6404: val local_default_proof = local_terminal_proof default_text; wenzelm@5824: wenzelm@6404: fun global_qed alt_name alt_atts opt_text = wenzelm@6404: Proof.global_qed (refine (if_none opt_text finish_text)) alt_name alt_atts; wenzelm@5824: wenzelm@6404: fun global_terminal_proof text = Seq.hd o Seq.map (global_qed None None None) o proof (Some text); wenzelm@6404: val global_immediate_proof = global_terminal_proof (Basic (K same)); wenzelm@6404: val global_default_proof = global_terminal_proof default_text; wenzelm@5824: wenzelm@5824: wenzelm@5824: wenzelm@5824: (** theory setup **) wenzelm@5824: 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@6108: ("same", no_args same, "insert facts, nothing else"), wenzelm@5824: ("assumption", no_args assumption, "proof by assumption"), wenzelm@5824: ("finish", no_args asm_finish, "finish proof by assumption"), wenzelm@6532: ("fold", thms_args fold, "fold definitions"), wenzelm@6532: ("unfold", thms_args unfold, "unfold definitions"), wenzelm@5884: ("rule", thms_args rule, "apply primitive rule")]; wenzelm@5824: wenzelm@5824: wenzelm@5824: (* setup *) wenzelm@5824: wenzelm@5824: val setup = [MethodsData.init, add_methods pure_methods]; wenzelm@5824: wenzelm@5824: wenzelm@5824: end; wenzelm@5824: wenzelm@5824: wenzelm@5824: structure BasicMethod: BASIC_METHOD = Method; wenzelm@5824: open BasicMethod;