# HG changeset patch # User wenzelm # Date 1183475833 -7200 # Node ID 438e5c4ef2c0b8c7e875d58ddd093fb77c61914a # Parent ecf487dce798637f9d3e9163db7962600c13a69f added CONVERSION tactical; tuned signature; diff -r ecf487dce798 -r 438e5c4ef2c0 src/Pure/tctical.ML --- a/src/Pure/tctical.ML Tue Jul 03 17:17:11 2007 +0200 +++ b/src/Pure/tctical.ML Tue Jul 03 17:17:13 2007 +0200 @@ -10,68 +10,67 @@ infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE'; infix 0 THEN_ELSE; - signature TACTICAL = sig - type tactic (* = thm -> thm Seq.seq*) - val all_tac : tactic - val ALLGOALS : (int -> tactic) -> tactic - val APPEND : tactic * tactic -> tactic - val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic - val CHANGED : tactic -> tactic - val CHANGED_PROP : tactic -> tactic - val CHANGED_GOAL : (int -> tactic) -> int -> tactic - val COND : (thm -> bool) -> tactic -> tactic -> tactic - val DETERM : tactic -> tactic - val EVERY : tactic list -> tactic - val EVERY' : ('a -> tactic) list -> 'a -> tactic - val EVERY1 : (int -> tactic) list -> tactic - val FILTER : (thm -> bool) -> tactic -> tactic - val FIRST : tactic list -> tactic - val FIRST' : ('a -> tactic) list -> 'a -> tactic - val FIRST1 : (int -> tactic) list -> tactic - val FIRSTGOAL : (int -> tactic) -> tactic - val INTLEAVE : tactic * tactic -> tactic - val INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic - val METAHYPS : (thm list -> tactic) -> int -> tactic - val metahyps_thms : int -> thm -> thm list option - val no_tac : tactic - val ORELSE : tactic * tactic -> tactic - val ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic - val pause_tac : tactic - val print_tac : string -> tactic - val PRIMITIVE : (thm -> thm) -> tactic - val PRIMSEQ : (thm -> thm Seq.seq) -> tactic - val RANGE : (int -> tactic) list -> int -> tactic - val REPEAT : tactic -> tactic - val REPEAT1 : tactic -> tactic - val REPEAT_FIRST : (int -> tactic) -> tactic - val REPEAT_SOME : (int -> tactic) -> tactic - val REPEAT_DETERM_N : int -> tactic -> tactic - val REPEAT_DETERM : tactic -> tactic - val REPEAT_DETERM1 : tactic -> tactic + type tactic = thm -> thm Seq.seq + val THEN: tactic * tactic -> tactic + val ORELSE: tactic * tactic -> tactic + val APPEND: tactic * tactic -> tactic + val INTLEAVE: tactic * tactic -> tactic + val THEN_ELSE: tactic * (tactic*tactic) -> tactic + val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic + val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic + val APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic + val INTLEAVE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic + val all_tac: tactic + val no_tac: tactic + val DETERM: tactic -> tactic + val COND: (thm -> bool) -> tactic -> tactic -> tactic + val TRY: tactic -> tactic + val EVERY: tactic list -> tactic + val EVERY': ('a -> tactic) list -> 'a -> tactic + val EVERY1: (int -> tactic) list -> tactic + val FIRST: tactic list -> tactic + val FIRST': ('a -> tactic) list -> 'a -> tactic + val FIRST1: (int -> tactic) list -> tactic + val RANGE: (int -> tactic) list -> int -> tactic + val print_tac: string -> tactic + val pause_tac: tactic + val trace_REPEAT: bool ref + val suppress_tracing: bool ref + val tracify: bool ref -> tactic -> tactic + val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic + val DETERM_UNTIL: (thm -> bool) -> tactic -> tactic + val REPEAT_DETERM_N: int -> tactic -> tactic + val REPEAT_DETERM: tactic -> tactic + val REPEAT: tactic -> tactic + val REPEAT_DETERM1: tactic -> tactic + val REPEAT1: tactic -> tactic + val FILTER: (thm -> bool) -> tactic -> tactic + val CHANGED: tactic -> tactic + val CHANGED_PROP: tactic -> tactic + val ALLGOALS: (int -> tactic) -> tactic + val SOMEGOAL: (int -> tactic) -> tactic + val FIRSTGOAL: (int -> tactic) -> tactic + val REPEAT_SOME: (int -> tactic) -> tactic + val REPEAT_DETERM_SOME: (int -> tactic) -> tactic + val REPEAT_FIRST: (int -> tactic) -> tactic val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic - val REPEAT_DETERM_SOME: (int -> tactic) -> tactic - val DETERM_UNTIL : (thm -> bool) -> tactic -> tactic - val SINGLE : tactic -> thm -> thm option - val SOMEGOAL : (int -> tactic) -> tactic - val strip_context : term -> (string * typ) list * term list * term - val CSUBGOAL : ((cterm * int) -> tactic) -> int -> tactic - val SUBGOAL : ((term * int) -> tactic) -> int -> tactic - val suppress_tracing : bool ref - val THEN : tactic * tactic -> tactic - val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic - val THEN_ALL_NEW : (int -> tactic) * (int -> tactic) -> int -> tactic - val REPEAT_ALL_NEW : (int -> tactic) -> int -> tactic - val THEN_ELSE : tactic * (tactic*tactic) -> tactic - val traced_tac : (thm -> (thm * thm Seq.seq) option) -> tactic - val tracify : bool ref -> tactic -> tactic - val trace_REPEAT : bool ref - val TRY : tactic -> tactic - val TRYALL : (int -> tactic) -> tactic + val TRYALL: (int -> tactic) -> tactic + val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic + val SUBGOAL: ((term * int) -> tactic) -> int -> tactic + val CHANGED_GOAL: (int -> tactic) -> int -> tactic + val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic + val REPEAT_ALL_NEW: (int -> tactic) -> int -> tactic + val strip_context: term -> (string * typ) list * term list * term + val metahyps_thms: int -> thm -> thm list option + val METAHYPS: (thm list -> tactic) -> int -> tactic + val PRIMSEQ: (thm -> thm Seq.seq) -> tactic + val PRIMITIVE: (thm -> thm) -> tactic + val SINGLE: tactic -> thm -> thm option + val CONVERSION: conv -> int -> tactic end; - structure Tactical : TACTICAL = struct @@ -519,9 +518,13 @@ (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*) fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun); -(* Inverse (more or less) of PRIMITIVE *) +(*Inverse (more or less) of PRIMITIVE*) fun SINGLE tacf = Option.map fst o Seq.pull o tacf +(*Conversions as tactics*) +fun CONVERSION cv i st = Seq.single (Conv.goal_conv_rule cv i st) + handle THM _ => Seq.empty | CTERM _ => Seq.empty; + end; open Tactical;