Re: [isabelle] Uniqueness quantification



I indeed want "p q" to hold for exactly one of the 5 expressions, i.e.
only one of the 5 predicates returns true for all arguments.

Applying clarify/clarsimp seems to work indeed. However, if I change
the type of the predicates from "nat =>  bool" to "(nat*nat) =>  bool",
the proof breaks. Do you know why the input type of the predicates
affects the proof?

No particularly good ideas here, except that things are becoming more complicated.

Right, but how come the reverse doesn't hold? If there's exactly one
of the predicates returning true, then isn't the length of the
filtered list one?

No. To phrase what I said before in different language again, the cardinality of the set you've been talking about "{p1, p2, p3, p4, p5}" isn't necessarily 5. If "p1 = p2" then there are less than 5 unique elements of the set "{p1, p2, p3, p4, p5}".

To rephrase this once more: if you add a p6 to your axiomatization with the axiom ax6: "p6 = p5", then the equivalent lemma is still provable:

lemma lem: "EX! p:{p1,p2,p3,p4,p5, p6}. p q"
apply (simp add: conj_disj_distribR Ex1_def all_conj_distrib ex_disj_distrib)
  apply clarsimp
  apply (metis axs)
  done

The reason this is provable is because "{p1, p2, p3, p4, p5, p6} = {p1, p2, p3, p4, p5}", so it's really just the same as the 5 example.

Yours,
    Thomas.





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