summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Sequents/LK.thy

author | wenzelm |

Thu Dec 07 00:42:04 2006 +0100 (2006-12-07) | |

changeset 21687 | f689f729afab |

parent 21428 | f84cf8e9cad8 |

child 27149 | 123377499a8e |

permissions | -rw-r--r-- |

reorganized structure Goal vs. Tactic;

1 (* Title: LK/LK.ML

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 1993 University of Cambridge

6 Axiom to express monotonicity (a variant of the deduction theorem). Makes the

7 link between |- and ==>, needed for instance to prove imp_cong.

9 Axiom left_cong allows the simplifier to use left-side formulas. Ideally it

10 should be derived from lower-level axioms.

12 CANNOT be added to LK0.thy because modal logic is built upon it, and

13 various modal rules would become inconsistent.

14 *)

16 theory LK

17 imports LK0

18 uses ("simpdata.ML")

19 begin

21 axioms

23 monotonic: "($H |- P ==> $H |- Q) ==> $H, P |- Q"

25 left_cong: "[| P == P'; |- P' ==> ($H |- $F) == ($H' |- $F') |]

26 ==> (P, $H |- $F) == (P', $H' |- $F')"

28 use "simpdata.ML"

30 end