[isabelle] "apply auto" transforms provable statement to something false?
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