summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 28 Jul 1999 13:45:33 +0200 | |

changeset 7117 | 37eccadf6b8a |

parent 7116 | 8c1caac3e54e |

child 7118 | ee384c7b7416 |

congruence rule for |-

--- a/src/Sequents/LK.thy Wed Jul 28 13:42:20 1999 +0200 +++ b/src/Sequents/LK.thy Wed Jul 28 13:45:33 1999 +0200 @@ -6,6 +6,9 @@ Axiom to express monotonicity (a variant of the deduction theorem). Makes the link between |- and ==>, needed for instance to prove imp_cong. +Axiom left_cong allows the simplifier to use left-side formulas. Ideally it +should be derived from lower-level axioms. + CANNOT be added to LK0.thy because modal logic is built upon it, and various modal rules would become inconsistent. *) @@ -16,4 +19,6 @@ monotonic "($H |- P ==> $H |- Q) ==> $H, P |- Q" + left_cong "[| P == P'; |- P' ==> ($H |- $F) == ($H' |- $F') |] + ==> (P, $H |- $F) == (P', $H' |- $F')" end