Re: [isabelle] Generalized elimination rule?



Peter Lammich wrote:
Hi Brian,

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?

Best,
 Peter

Dear Peter,

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.

Regards,

Jeremy


consts
  meta_keep     :: "bool => prop => prop"

defs
  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 MHonArc.