# HG changeset patch # User paulson # Date 865511563 -7200 # Node ID c0466958df5dd090cba33bb0cbb2058dee1762d3 # Parent 98a2d517cabe63999f8ff09c554b3060447cd94b Tidying of signature. More robust renaming in freeze_thaw. New tactic distinct_subgoals_tac diff -r 98a2d517cabe -r c0466958df5d src/Pure/tactic.ML --- a/src/Pure/tactic.ML Thu Jun 05 13:30:24 1997 +0200 +++ b/src/Pure/tactic.ML Thu Jun 05 13:52:43 1997 +0200 @@ -8,82 +8,84 @@ signature TACTIC = sig - val ares_tac: thm list -> int -> tactic + val ares_tac : thm list -> int -> tactic val asm_rewrite_goal_tac: bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic - val assume_tac: int -> tactic - val atac: int ->tactic + val assume_tac : int -> tactic + val atac : int ->tactic val bimatch_from_nets_tac: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic - val bimatch_tac: (bool*thm)list -> int -> tactic + val bimatch_tac : (bool*thm)list -> int -> tactic val biresolve_from_nets_tac: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic - val biresolve_tac: (bool*thm)list -> int -> tactic - val build_net: thm list -> (int*thm) Net.net + val biresolve_tac : (bool*thm)list -> int -> tactic + val build_net : thm list -> (int*thm) Net.net val build_netpair: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net - val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic - val compose_tac: (bool * thm * int) -> int -> tactic - val cut_facts_tac: thm list -> int -> tactic - val cut_inst_tac: (string*string)list -> thm -> int -> tactic - val defer_tac : int -> tactic - val dmatch_tac: thm list -> int -> tactic - val dresolve_tac: thm list -> int -> tactic - val dres_inst_tac: (string*string)list -> thm -> int -> tactic - val dtac: thm -> int ->tactic - val etac: thm -> int ->tactic - val eq_assume_tac: int -> tactic - val ematch_tac: thm list -> int -> tactic - val eresolve_tac: thm list -> int -> tactic - val eres_inst_tac: (string*string)list -> thm -> int -> tactic - val filter_thms: (term*term->bool) -> int*term*thm list -> thm list - val filt_resolve_tac: thm list -> int -> int -> tactic - val flexflex_tac: tactic - val fold_goals_tac: thm list -> tactic - val fold_tac: thm list -> tactic - val forward_tac: thm list -> int -> tactic - val forw_inst_tac: (string*string)list -> thm -> int -> tactic - val freeze_thaw: thm -> thm * (thm -> thm) - val insert_tagged_brl: ('a*(bool*thm)) * - (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) -> - ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net - val delete_tagged_brl: (bool*thm) * - ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) -> + val compose_inst_tac : (string*string)list -> (bool*thm*int) -> + int -> tactic + val compose_tac : (bool * thm * int) -> int -> tactic + val cut_facts_tac : thm list -> int -> tactic + val cut_inst_tac : (string*string)list -> thm -> int -> tactic + val defer_tac : int -> tactic + val distinct_subgoals_tac : tactic + val dmatch_tac : thm list -> int -> tactic + val dresolve_tac : thm list -> int -> tactic + val dres_inst_tac : (string*string)list -> thm -> int -> tactic + val dtac : thm -> int ->tactic + val etac : thm -> int ->tactic + val eq_assume_tac : int -> tactic + val ematch_tac : thm list -> int -> tactic + val eresolve_tac : thm list -> int -> tactic + val eres_inst_tac : (string*string)list -> thm -> int -> tactic + val filter_thms : (term*term->bool) -> int*term*thm list -> thm list + val filt_resolve_tac : thm list -> int -> int -> tactic + val flexflex_tac : tactic + val fold_goals_tac : thm list -> tactic + val fold_tac : thm list -> tactic + val forward_tac : thm list -> int -> tactic + val forw_inst_tac : (string*string)list -> thm -> int -> tactic + val freeze_thaw : thm -> thm * (thm -> thm) + val insert_tagged_brl : ('a*(bool*thm)) * + (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) -> + ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net + val delete_tagged_brl : (bool*thm) * + ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) -> (int*(bool*thm))Net.net * (int*(bool*thm))Net.net - val is_fact: thm -> bool - val lessb: (bool * thm) * (bool * thm) -> bool - val lift_inst_rule: thm * int * (string*string)list * thm -> thm - val make_elim: thm -> thm - val match_from_net_tac: (int*thm) Net.net -> int -> tactic - val match_tac: thm list -> int -> tactic - val metacut_tac: thm -> int -> tactic - val net_bimatch_tac: (bool*thm) list -> int -> tactic - val net_biresolve_tac: (bool*thm) list -> int -> tactic - val net_match_tac: thm list -> int -> tactic - val net_resolve_tac: thm list -> int -> tactic - val orderlist: (int * 'a) list -> 'a list - val PRIMITIVE: (thm -> thm) -> tactic - val PRIMSEQ: (thm -> thm Sequence.seq) -> tactic - val prune_params_tac: tactic - val rename_tac: string -> int -> tactic - val rename_last_tac: string -> string list -> int -> tactic - val resolve_from_net_tac: (int*thm) Net.net -> int -> tactic - val resolve_tac: thm list -> int -> tactic - val res_inst_tac: (string*string)list -> thm -> int -> tactic - val rewrite_goals_tac: thm list -> tactic - val rewrite_tac: thm list -> tactic - val rewtac: thm -> tactic - val rotate_tac: int -> int -> tactic - val rtac: thm -> int -> tactic - val rule_by_tactic: tactic -> thm -> thm - val subgoal_tac: string -> int -> tactic - val subgoals_tac: string list -> int -> tactic - val subgoals_of_brl: bool * thm -> int - val term_lift_inst_rule: + val is_fact : thm -> bool + val lessb : (bool * thm) * (bool * thm) -> bool + val lift_inst_rule : thm * int * (string*string)list * thm -> thm + val make_elim : thm -> thm + val match_from_net_tac : (int*thm) Net.net -> int -> tactic + val match_tac : thm list -> int -> tactic + val metacut_tac : thm -> int -> tactic + val net_bimatch_tac : (bool*thm) list -> int -> tactic + val net_biresolve_tac : (bool*thm) list -> int -> tactic + val net_match_tac : thm list -> int -> tactic + val net_resolve_tac : thm list -> int -> tactic + val orderlist : (int * 'a) list -> 'a list + val PRIMITIVE : (thm -> thm) -> tactic + val PRIMSEQ : (thm -> thm Sequence.seq) -> tactic + val prune_params_tac : tactic + val rename_tac : string -> int -> tactic + val rename_last_tac : string -> string list -> int -> tactic + val resolve_from_net_tac : (int*thm) Net.net -> int -> tactic + val resolve_tac : thm list -> int -> tactic + val res_inst_tac : (string*string)list -> thm -> int -> tactic + val rewrite_goals_tac : thm list -> tactic + val rewrite_tac : thm list -> tactic + val rewtac : thm -> tactic + val rotate_tac : int -> int -> tactic + val rtac : thm -> int -> tactic + val rule_by_tactic : tactic -> thm -> thm + val subgoal_tac : string -> int -> tactic + val subgoals_tac : string list -> int -> tactic + val subgoals_of_brl : bool * thm -> int + val term_lift_inst_rule : thm * int * (indexname*typ)list * ((indexname*typ)*term)list * thm -> thm - val thin_tac: string -> int -> tactic - val trace_goalno_tac: (int -> tactic) -> int -> tactic + val thin_tac : string -> int -> tactic + val trace_goalno_tac : (int -> tactic) -> int -> tactic end; @@ -99,24 +101,25 @@ (*Convert all Vars in a theorem to Frees. Also return a function for - reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*) -local - fun string_of (a,0) = a - | string_of (a,i) = a ^ "_" ^ string_of_int i; -in - fun freeze_thaw th = - let val fth = freezeT th - val vary = variant (add_term_names (#prop(rep_thm fth), [])) - val {prop,sign,...} = rep_thm fth - fun mk_inst (Var(v,T)) = - (cterm_of sign (Var(v,T)), - cterm_of sign (Free(vary (string_of v), T))) - val insts = map mk_inst (term_vars prop) - fun thaw th' = - th' |> forall_intr_list (map #2 insts) - |> forall_elim_list (map #1 insts) - in (instantiate ([],insts) fth, thaw) end; -end; + reversing that operation. DOES NOT WORK FOR TYPE VARIABLES. + Similar code in type/freeze_thaw*) +fun freeze_thaw th = + let val fth = freezeT th + val {prop,sign,...} = rep_thm fth + val used = add_term_names (prop, []) + and vars = term_vars prop + fun newName (Var(ix,_), (pairs,used)) = + let val v = variant used (string_of_indexname ix) + in ((ix,v)::pairs, v::used) end; + val (alist, _) = foldr newName (vars, ([], used)) + fun mk_inst (Var(v,T)) = + (cterm_of sign (Var(v,T)), + cterm_of sign (Free(the (assoc(alist,v)), T))) + val insts = map mk_inst vars + fun thaw th' = + th' |> forall_intr_list (map #2 insts) + |> forall_elim_list (map #1 insts) + in (instantiate ([],insts) fth, thaw) end; (*Rotates the given subgoal to be the last. Useful when re-playing @@ -202,6 +205,21 @@ (*Smash all flex-flex disagreement pairs in the proof state.*) val flexflex_tac = PRIMSEQ flexflex_rule; + +(*Remove duplicate subgoals. By Mark Staples*) +local +fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b); +in +fun distinct_subgoals_tac state = + let val (frozth,thawfn) = freeze_thaw state + val froz_prems = cprems_of frozth + val assumed = implies_elim_list frozth (map assume froz_prems) + val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems) + assumed; + in Sequence.single (thawfn implied) end +end; + + (*Lift and instantiate a rule wrt the given state and subgoal number *) fun lift_inst_rule (st, i, sinsts, rule) = let val {maxidx,sign,...} = rep_thm st