Re: [isabelle] Problems with `drule` and `erule` in the presence of chained facts



Hi Wolfgang,

Although there might be better solutions and deeper understandings, my usual quick and dirty ways are:

  lemma "P ∧ Q ⟹ R"
     using TrueI
     apply -
     apply (drule conjunct1)
     oops

Or 

  lemma "P ∧ Q ⟹ R"
     using TrueI
     apply (drule_tac conjunct1)
     oops

Wenda

> On 13 Jul 2019, at 16:17, Wolfgang Jeltsch <wolfgang-it at jeltsch.info> wrote:
> 
> Hi!
> 
> I’m developing a proof method that involves applications of `drule`.
> This proof methods doesn’t work in the presence of chained facts,
> because its `drule` invocations fail in this situation.
> 
> Consider the following minimal example code:
> 
>    lemma "P ∧ Q ⟹ R"
>      apply (drule conjunct1)
>      oops
> 
> The invocation of `drule` correctly turns the goal into `P ⟹ R`.
> However, it fails in the following situation:
> 
>    lemma "P ∧ Q ⟹ R"
>      using TrueI
>      apply (drule conjunct1)
>      oops
> 
> Why is that, and how can `drule` been made work also in the presence of
> chained facts?
> 
> I also tried to use `erule` instead of `drule`, but the same problem
> occurred with that.
> 
> In my use case, I actually want to turn all chained facts into goal
> premises anyhow. I can add the chained facts to the list of goal
> premises by invoking `insert method_facts`, but this leaves the chained
> facts in place, so that the problem with `drule` remains. Is there
> perhaps a proof method that removes all chained facts?
> 
> I know that `simp` turns chained facts into goal premises. Therefore, my
> current workaround is to invoke `simp` in a way where it essentially
> doesn’t rewrite anything but only moves chained facts into the goal. To
> this end, I’m using `(insert TrueI, simp only: True_implies_equals)`. This has the side effect of removing all previously existing
> `True` premises, but this isn’t a problem in my use case. Still, I’d be
> happy to use a cleaner solution.
> 
> All the best,
> Wolfgang
> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.