Stream: Beginner Questions

Topic: substitution from assumptions, choosing which one you want

Chengsong Tan (Nov 18 2023 at 17:44):

Hi,

I am trying to use the erule ssubst command
to use an equality from the assumption
to do a rewriting to the goal,
but I can't get Isabelle to select the second rather than the first assumption to do that
rewriting:

theory Example imports Main begin
fun Lexists_nonEmpty :: "'a list ⇒ ('a ⇒ bool) ⇒ bool" where
  "Lexists_nonEmpty [] p  = False"
| "Lexists_nonEmpty [a] p = (p a)"
| "Lexists_nonEmpty (a # as) p = (p a ∨ Lexists_nonEmpty as p)"


lemma Lexists_nonEmpty_concat: shows "Lexists_nonEmpty (rs @ rs2) p = (Lexists_nonEmpty rs p ∨ Lexists_nonEmpty rs2 p)"

  apply(induct rs  )
   apply simp+
  apply(subgoal_tac "Lexists_nonEmpty (a # rs @ rs2) p = p a ∨ Lexists_nonEmpty (rs @ rs2) p")
  apply(erule ssubst(2))


  sorry

end

Any ideas?

thanks a lot!
Chengsong

Mathias Fleury (Nov 18 2023 at 17:48):

First: ssubst(2) means the second theorem of ssubst, like in every context

Mathias Fleury (Nov 18 2023 at 17:51):

Second: you can reorder assumptions with rotate_tac

Mathias Fleury (Nov 18 2023 at 17:51):

Third: it makes no difference here, because only one assumption is an equality. So I do not get what you are trying to achieve

Mathias Fleury (Nov 18 2023 at 17:53):

Lexists_nonEmpty (rs @ rs2) p = (Lexists_nonEmpty rs p ∨ Lexists_nonEmpty rs2 p) ⟹
       Lexists_nonEmpty (a # rs @ rs2) p = p a ∨ Lexists_nonEmpty (rs @ rs2) p ⟹
       Lexists_nonEmpty (a # rs @ rs2) p = (Lexists_nonEmpty (a # rs) p ∨ Lexists_nonEmpty rs2 p)

Chengsong Tan (Nov 18 2023 at 18:00):

Mathias Fleury said:

Third: it makes no difference here, because only one assumption is an equality. So I do not get what you are trying to achieve

Hi Mathias,

I was trying to use the equality which I just inserted using subgoal_tac, namely

Lexists_nonEmpty (a # rs @ rs2) p = p a ∨ Lexists_nonEmpty (rs @ rs2) p

Chengsong Tan (Nov 18 2023 at 18:02):

So I would like to turn the LHS Lexists_nonEmpty (a # rs @ rs2) p into p a \/ .......

Chengsong Tan (Nov 18 2023 at 18:06):

(Using bracket mode) the proof state looks like this:

proof (prove)
goal (2 subgoals):
 1. ⋀a rs.
       ⟦Lexists_nonEmpty (rs @ rs2) p = (Lexists_nonEmpty rs p ∨ Lexists_nonEmpty rs2 p);
        Lexists_nonEmpty (a # rs @ rs2) p = p a ∨ Lexists_nonEmpty (rs @ rs2) p⟧
       ⟹ Lexists_nonEmpty (a # rs @ rs2) p = (Lexists_nonEmpty (a # rs) p ∨ Lexists_nonEmpty rs2 p)
.......

so I am a bit puzzled why after erule ssubst the inductive hypothesis got deleted instead of the second premise in this proof state.

Mathias Fleury (Nov 18 2023 at 18:19):

This Lexists_nonEmpty (a # rs @ rs2) p = p a ∨ Lexists_nonEmpty (rs @ rs2) p is (_ = _) ∨ _

Mathias Fleury (Nov 18 2023 at 18:19):

So no equality here

Mathias Fleury (Nov 18 2023 at 18:21):

erule always eliminates the assumption.

Mathias Fleury (Nov 18 2023 at 18:22):

erule is here looking at all the possible assumptions (there is only one), instantiate the theorem and rewrites it. As it is HO unification, the term ?s does not appear in the goal, so the function is (%_. x) ?s and you do not see any difference

Mathias Fleury (Nov 18 2023 at 18:23):

If you try

lemma Lexists_nonEmpty_concat: shows "Lexists_nonEmpty (rs @ rs2) p = (Lexists_nonEmpty rs p ∨ Lexists_nonEmpty rs2 p)"

  apply(induct rs  )
   apply simp+
  apply(subgoal_tac "Lexists_nonEmpty (a # rs @ rs2) p = (p a ∨ Lexists_nonEmpty (rs @ rs2) p)")
   apply(erule ssubst)

you will see the rewriting making more sense

Chengsong Tan (Nov 18 2023 at 19:51):

Mathias Fleury said:

So no equality here

Nicely spotted

Chengsong Tan (Nov 18 2023 at 19:59):

Mathias Fleury said:

erule is here looking at all the possible assumptions (there is only one), instantiate the theorem and rewrites it. As it is HO unification, the term ?s does not appear in the goal, so the function is (%_. x) ?s and you do not see any difference

Sorry if this seems obvious but which term are you referring to is (%_. x) ?s?

Mathias Fleury (Nov 18 2023 at 21:01):

The function in the conclusion of ssubst rule

Chengsong Tan (Nov 19 2023 at 12:08):

[Quoting…]

Just to rephrase it to double-check my understanding,
the x means the term Lexists_nonEmpty (rs @ rs2) p = (Lexists_nonEmpty (a # rs) p \/ Lexists_nonEmpty rs2 p) right?
And ?s and ?t have been instantiated to the LHS and RHS of the I.H., though they are discarded by the function and therefore the output remains to be x.

Mathias Fleury (Nov 19 2023 at 12:25):

yes exactly

Last updated: Apr 28 2024 at 01:11 UTC