Questions tagged [apply-script]

Let's say I have a lemma about a simple inductively-defined set: inductive_set foo :: "'a ⇒ 'a list set" for x :: 'a where "[] ∈ foo x" | "[x] ∈ foo x" lemma "⋀x y. y ∈ foo x ⟹ qux x y ⟹ baz x y" (It's important to me that the "⋀x y" bit stays,…

Say I have a lemma mylem: foo ?a = bar ?a, and I need to apply it on a goal that has two occurrences of foo, e.g. baz (foo (f p q)) (foo (g r s)), but only at one of these positions. I know of two ways of doing that without having to write out all…

If my goal state is foo ==> bar --> qux, I know that I can use the statement apply (intro impI) to yield the goal state foo ==> bar ==> qux. What about the other direction? Which command will send me back to the goal state foo ==> bar --> qux?…