Re: [isabelle] I need a meta-or



On Thu, 25 Jul 2013, Gottfried Barrow wrote:

There's the meta-and, &&&, but I need a meta-or, so I don't have to define two meta-or operators to keep from using PROP.

If there's a &&&, then it seems there should be the complete suite of basic meta operators

In principle you could define all the standard connectives of Isabelle/HOL in Isabelle/Pure as well, but what is the point?

The purpose of Isabelle/Pure is to provide a framework for higher-order natural deduction, with declarative rule structure indicated by the connectives !! and ==> (i.e. Minimal Higher-order Logic). Anything beyond that is not really pure.


Note that &&& is merely used internally as auxilary device -- it should hardly ever occur in applications of Isabelle/Pure (or HOL). You just use multiple propositions directly in Isar like this:

  lemma A and B and C
  proof -
    show A sorry
    show B sorry
    show C sorry
  qed

You better chose to ignore that the internal system state somewhere involves "A &&& B &&& C" -- it is never encountered in a regular proof.


	Makarius




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