Re: [isabelle] Generalized elimination rule?
Peter Lammich wrote:
Many thanks you for your answer.
I adopted your proposal for my needs. However, I ran into a problem
that should also be imminent in your proposal (?).
If there are premises of the form !!x. _==>_, they are counted in
nhyps, however dtac keepI will not unify against them, thus
val ktac = EVERY' (replicate nhyps (dtac keepI)) : int -> tactic ;
produces premises that are doubly-wrapped into keep.
What's the best way around?
Only counting "plain" premises? (How?)
Can keepI be defined to also wrap higher-order premises?
I'm not quite sure if I understand you correctly.
Are you talking about the situation where there is a premise (among the
list of premises of a subgoal) of the form !!x. _==>_ ?
(Isn't this rather unusual - could I see an example of how this arises ?)
Certainly, keep, as I defined it, won't wrap around a premise of the form
!!x. _==>_ because such a premise is of type prop, not bool.
Isabelle generally - I think - wasn't intended to work very much with
meta-level stuff, and previously I have found that playing around with
meta-level props instead of object level bools doesn't seem to work as
expected. However to my surprise the attached does seem to work - try
it out and see if it works on your problem example.
meta_keep :: "bool => prop => prop"
meta_keep_def : "meta_keep b f == f"
val meta_iffD2 = prove_goal ProtoPure.thy
"[| PROP P==PROP Q; PROP Q |] ==> PROP P"
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
val meta_iffD1 = symmetric_thm RS meta_iffD2;
val meta_iffDs = [meta_iffD1, meta_iffD2] ;
val _ = ListPair.app bind_thm (["meta_keepD", "meta_keepI"],
[meta_keep_def] RL meta_iffDs) ;
val _ = bind_thm ("meta_keepTD",
read_instantiate [("b", "True")] meta_keepD) ;
val _ = bind_thm ("meta_keepFD",
read_instantiate [("b", "False")] meta_keepD) ;
val _ = bind_thm ("meta_keepF_thin", meta_keepFD RS thin_rl) ;
(* meta_fetac : thm -> int -> int -> tactic
like fatac n but also deletes hypotheses matched *)
fun meta_fetac th n sg st =
let val fth = thin_rl RS (replicate n meta_keepFD MRS th) : thm ;
val subgoal = List.nth (prems_of st, sg - 1) : term ;
(* turn all subgoal hypotheses H into meta_keep ?b H *)
val nhyps = length (Logic.strip_assums_hyp subgoal) ;
val ktac = EVERY' (replicate nhyps (dtac meta_keepI)) : int -> tactic ;
(* then apply ftac fth - see later *)
(* then apply atac n times,
which marks the hypotheses to be deleted with meta_keep False *)
val atacs = EVERY' (replicate n atac) ;
(* treat other instances of meta_keep ?b as meta_keep True, and erase *)
val ekttac = REPEAT o dtac meta_keepTD : int -> tactic ;
(* delete hypotheses which are (meta_keep False ...) *)
val ekftac = REPEAT o etac meta_keepF_thin : int -> tactic ;
(* combine all the above *)
val ctac = EVERY' [ktac, ftac fth, atacs] THEN_ALL_NEW
(ekttac THEN' ekftac) : int -> tactic ;
in ctac sg st end ;
This archive was generated by a fusion of
Pipermail (Mailman edition) and