[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:

    lemma bij_betw_Arr_arr:
    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 *)

      using arr_char
      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
provable goals.

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 MHonArc.