Re: [isabelle] "apply auto" transforms provable statement to something false?
It is normal behaviour that auto transforms a provable goal into something unprovable.
This happens particularly often if (1) you have declared a rule as safe (intro!, elim!,
dest!) which is actually not safe or (2) your subgoals contain schematic variables (?x).
The latter may be the reason in your case because the "intro bij_betwI" introduces the
schematic variable ?g in your goal state.
On 25/01/16 12:02, Eugene W. Stark wrote:
I was surprised by this, and I was wondering if it is supposed to be able to happen.
I have the following lemma:
shows "bij_betw Some (Collect Arr) (Collect C.arr)"
I can prove it in two ways:
proof (intro bij_betwI)
show "Some â Collect Arr â Collect C.arr" using arr_char by auto
show "the â Collect C.arr â Collect Arr" using arr_char by auto
show "âx. x â Collect Arr â the (Some x) = x" by auto
show "ây. y â Collect C.arr â Some (the y) = y" using arr_char by auto
qed (* Succeeds *)
by (smt bij_betwI' mem_Collect_eq option.collapse option.distinct(1) option.sel)
(* Succeeds *)
However, the following fails:
apply (intro bij_betwI) using arr_char apply auto (* subgoal appears false *)
try (* Nitpick produces counterexample *)
For some reason, I had in my mind that auto should not produce false subgoals from
By the way, the lemma occurs in a locale context, but I have elsewhere shown the
locale consistent by exhibiting a concrete interpretation. So it is not the case
that the locale assumptions are inconsistent.
- Gene Stark
This archive was generated by a fusion of
Pipermail (Mailman edition) and