# HG changeset patch # User wenzelm # Date 978899771 -3600 # Node ID 083d4a6734b4e3efce90468edca67feecbb2e95c # Parent 8b2eafed618352bc0314ef8b71fc0eecd139a40a tuned norm_hhf(_tac); diff -r 8b2eafed6183 -r 083d4a6734b4 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Sun Jan 07 21:35:34 2001 +0100 +++ b/src/Pure/tactic.ML Sun Jan 07 21:36:11 2001 +0100 @@ -13,51 +13,51 @@ bool*bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic val assume_tac : int -> tactic val atac : int ->tactic - val bimatch_from_nets_tac: + 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 biresolution_from_nets_tac: + val biresolution_from_nets_tac: ('a list -> (bool * thm) list) -> bool -> 'a Net.net * 'a Net.net -> int -> tactic - val biresolve_from_nets_tac: + 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 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) -> + val compose_inst_tac : (string*string)list -> (bool*thm*int) -> int -> tactic - val compose_tac : (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 cut_inst_tac : (string*string)list -> thm -> int -> tactic val datac : thm -> int -> 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 dres_inst_tac : (string*string)list -> thm -> int -> tactic val dtac : thm -> int ->tactic val eatac : thm -> int -> int -> tactic val etac : thm -> int ->tactic - val eq_assume_tac : 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 fatac : thm -> int -> int -> tactic - val filter_prems_tac : (term -> bool) -> int -> tactic + val filter_prems_tac : (term -> bool) -> 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_rule : thm list -> thm -> thm val fold_tac : thm list -> tactic - val forward_tac : thm list -> int -> tactic + val forward_tac : thm list -> int -> tactic val forw_inst_tac : (string*string)list -> thm -> int -> tactic val ftac : thm -> int ->tactic - val insert_tagged_brl : ('a*(bool*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) * + 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 @@ -74,15 +74,15 @@ val norm_hhf : thm -> thm val norm_hhf_tac : int -> tactic val orderlist : (int * 'a) list -> 'a list - val PRIMITIVE : (thm -> thm) -> tactic - val PRIMSEQ : (thm -> thm Seq.seq) -> tactic + val PRIMITIVE : (thm -> thm) -> tactic + val PRIMSEQ : (thm -> thm Seq.seq) -> tactic val prune_params_tac : tactic val rename_params_tac : string list -> int -> 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 res_inst_tac : (string*string)list -> thm -> int -> tactic val rewrite_goal_tac : thm list -> int -> tactic val rewrite_goals_rule: thm list -> thm -> thm val rewrite_rule : thm list -> thm -> thm @@ -105,14 +105,14 @@ end; -structure Tactic : TACTIC = +structure Tactic : TACTIC = struct (*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) -fun trace_goalno_tac tac i st = +fun trace_goalno_tac tac i st = case Seq.pull(tac i st) of None => Seq.empty - | seqcell => (writeln ("Subgoal " ^ string_of_int i ^ " selected"); + | seqcell => (writeln ("Subgoal " ^ string_of_int i ^ " selected"); Seq.make(fn()=> seqcell)); (*Makes a rule by applying a tactic to an existing rule*) @@ -122,7 +122,7 @@ None => raise THM("rule_by_tactic", 0, [rl]) | Some(st',_) => Thm.varifyT (thaw st') end; - + (*** Basic tactics ***) (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*) @@ -194,14 +194,14 @@ local fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b); in -fun distinct_subgoals_tac state = +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 Seq.single (thawfn implied) end -end; +end; (*Lift and instantiate a rule wrt the given state and subgoal number *) @@ -214,7 +214,7 @@ and inc = maxidx+1 fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T) | liftvar t = raise TERM("Variable expected", [t]); - fun liftterm t = list_abs_free (params, + fun liftterm t = list_abs_free (params, Logic.incr_indexes(paramTs,inc) t) (*Lifts instantiation pair over params*) fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) @@ -264,7 +264,7 @@ subgoal. Fails if "i" is out of range. ***) (*compose version: arguments are as for bicompose.*) -fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st = +fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st = if i > nprems_of st then no_tac st else st |> (compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i @@ -289,10 +289,10 @@ (*For forw_inst_tac and dres_inst_tac. Preserve Var indexes of rl; increment revcut_rl instead.*) -fun make_elim_preserve rl = +fun make_elim_preserve rl = let val {maxidx,...} = rep_thm rl fun cvar ixn = cterm_of (Theory.sign_of ProtoPure.thy) (Var(ixn,propT)); - val revcut_rl' = + val revcut_rl' = instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl val arg = (false, rl, nprems_of rl) @@ -335,10 +335,10 @@ EVERY (map (fn th => metacut_tac th i) (filter is_fact ths)); (*Introduce the given proposition as a lemma and subgoal*) -fun subgoal_tac sprop i st = +fun subgoal_tac sprop i st = let val st' = Seq.hd (res_inst_tac [("psi", sprop)] cut_rl i st) val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i)) - in + in if null (term_tvars concl') then () else warning"Type variables in new subgoal: add a type constraint?"; Seq.single st' @@ -379,18 +379,18 @@ else x :: untaglist rest; (*return list elements in original order*) -fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls); +fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls); (*insert one tagged brl into the pair of nets*) fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) = - if eres then + if eres then case prems_of th of prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false)) | [] => error"insert_tagged_brl: elimination rule with no premises" else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet); (*build a pair of nets for biresolution*) -fun build_netpair netpair brls = +fun build_netpair netpair brls = foldr insert_tagged_brl (taglist 1 brls, netpair); (*delete one kbrl from the pair of nets; @@ -399,7 +399,7 @@ fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th') in fun delete_tagged_brl (brl as (eres,th), (inet,enet)) = - if eres then + if eres then case prems_of th of prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl)) | [] => (inet,enet) (*no major premise: ignore*) @@ -407,14 +407,14 @@ end; -(*biresolution using a pair of nets rather than rules. +(*biresolution using a pair of nets rather than rules. function "order" must sort and possibly filter the list of brls. boolean "match" indicates matching or unification.*) fun biresolution_from_nets_tac order match (inet,enet) = SUBGOAL (fn (prem,i) => let val hyps = Logic.strip_assums_hyp prem - and concl = Logic.strip_assums_concl prem + and concl = Logic.strip_assums_concl prem val kbrls = Net.unify_term inet concl @ List.concat (map (Net.unify_term enet) hyps) in PRIMSEQ (biresolution match (order kbrls) i) end); @@ -437,7 +437,7 @@ Net.insert_term ((concl_of th, krl), net, K false); (*build a net of rules for resolution*) -fun build_net rls = +fun build_net rls = foldr insert_krl (taglist 1 rls, Net.empty); (*resolution using a net rather than rules; pred supports filt_resolve_tac*) @@ -445,8 +445,8 @@ SUBGOAL (fn (prem,i) => let val krls = Net.unify_term net (Logic.strip_assums_concl prem) - in - if pred krls + in + if pred krls then PRIMSEQ (biresolution match (map (pair false) (orderlist krls)) i) else no_tac @@ -454,7 +454,7 @@ (*Resolve the subgoal using the rules (making a net) unless too flexible, which means more than maxr rules are unifiable. *) -fun filt_resolve_tac rules maxr = +fun filt_resolve_tac rules maxr = let fun pred krls = length krls <= maxr in filt_resolution_from_net_tac false pred (build_net rules) end; @@ -491,7 +491,7 @@ (*Rewrite subgoal i only. SELECT_GOAL avoids inefficiencies in goals_conv.*) fun asm_rewrite_goal_tac mode prover_tac mss = - SELECT_GOAL + SELECT_GOAL (PRIMITIVE (rewrite_goal_rule mode (result1 prover_tac) mss 1)); @@ -505,8 +505,13 @@ fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); fun rewtac def = rewrite_goals_tac [def]; -val norm_hhf = Drule.forall_elim_vars_safe o rewrite_rule [Drule.norm_hhf_eq]; -val norm_hhf_tac = rewrite_goal_tac [Drule.norm_hhf_eq]; +fun norm_hhf th = + (if Logic.is_norm_hhf (#prop (Thm.rep_thm th)) then th else rewrite_rule [Drule.norm_hhf_eq] th) + |> Drule.forall_elim_vars_safe; + +val norm_hhf_tac = SUBGOAL (fn (t, i) => + if Logic.is_norm_hhf t then all_tac + else rewrite_goal_tac [Drule.norm_hhf_eq] i); (*** for folding definitions, handling critical pairs ***) @@ -540,12 +545,12 @@ it affects nothing but the names of bound variables!*) fun rename_params_tac xs i = (if !Logic.auto_rename - then (warning "Resetting Logic.auto_rename"; + then (warning "Resetting Logic.auto_rename"; Logic.auto_rename := false) else (); PRIMITIVE (rename_params_rule (xs, i))); -fun rename_tac str i = - let val cs = Symbol.explode str in +fun rename_tac str i = + let val cs = Symbol.explode str in case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of [] => rename_params_tac (scanwords Symbol.is_letdig cs) i | c::_ => error ("Illegal character: " ^ c) @@ -553,7 +558,7 @@ (*Rename recent parameters using names generated from a and the suffixes, provided the string a, which represents a term, is an identifier. *) -fun rename_last_tac a sufs i = +fun rename_last_tac a sufs i = let val names = map (curry op^ a) sufs in if Syntax.is_identifier a then PRIMITIVE (rename_params_rule (names,i))