# 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.*