Re: [isabelle] successful attempt vs failed to apply initial proof method



> Is the above "exported rule" a fact, and, where does it come from? Can I use it to prove the goal, or it is a hypothetical fact that would prove the goal?

Let's say you need to show a HOL implication "A --> B".

lemma "A â B"
proof
 (* The proof command applies a standard rule. As a result,
    the state panel shows an unstructured goal state A â B. *)

  assume A
  show B
    sorry
qed

Do you agree that this is a syntactically correct proof "template"? This
is what the system tells you:

> Successful attempt to solve goal by exported rule

It could use the locally fixed variables, assumptions, and shown
propositions to (partly) discharge a subgoal in the goal state.

When you replace the "sorry" with a subproof which doesn't work, the
outer proof is still syntactically correct. But the system also tells
you that the subproof itself is incorrect ("Failed to apply ...").

It may help to think of Isar as a compiler with error recovery. Even if
a part of a program (= proof) does not type check, the compiler
"assumes" correctness and lets you go on with the rest. It'll only
report the error where it actually occurred.

Cheers
Lars




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