Re: [isabelle] I need a meta-or



I found a faster solution, so I don't know if I need what I asked for. However, it shows that a person might want to define a function using type prop, and not have to annotate everything with PROP, and need not to have to fight the automatic Trueprop coercion.

But I'm trying to duplicate the functionality of the right-hand side of a sequent without resorting to the object-logic operators.

According to pg.203 of isar-ref.pdf, if you have a sequent "A |- E, B, C, D", then you can negate all the right-hand side members except for one of them, and make a big implication out of it, with the non-negated member put to the far right, like "A ==> ~E ==> ~C ==> ~D ==> B".

So rather than implement the right-hand side as a meta-disjunction, I stay closer to what's in isar-ref.pdf. It's faster and acceptably meta. I have to use variables of type bool, along with False, which equals (!P. P), but the rest is ==>.

The simplifier seems to like working directly with True and False, rather than lower-level definitions.

I still have to use two operators:

notation ==> (infixr "|-" 4)

definition seqr :: "bool => bool => prop" (infixr "||" 15) where
  "seqr P Q == ((P ==> False) ==> Q)"
thm seqr_def

definition seql :: "bool => prop => prop" (infixr "|||" 15) where
  "seql P Q == ((P ==> False) ==> PROP Q)"
thm seql_def

theorem
  "   (A |- (~E ==> ~C ==> ~D ==> B))
  ==> (A |- (E ||| B ||| C || D))"
apply(auto simp only: seqr_def seql_def)
done

theorem
  "   (A |- (E ||| B ||| C || D))
  ==> (A |- (~E ==> ~C ==> ~D ==> B))"
apply(auto simp only: seqr_def seql_def)
done

It seems right.

Regards,
GB




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