equal
deleted
inserted
replaced
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Axiom to express monotonicity (a variant of the deduction theorem). Makes the |
6 Axiom to express monotonicity (a variant of the deduction theorem). Makes the |
7 link between |- and ==>, needed for instance to prove imp_cong. |
7 link between |- and ==>, needed for instance to prove imp_cong. |
|
8 |
|
9 Axiom left_cong allows the simplifier to use left-side formulas. Ideally it |
|
10 should be derived from lower-level axioms. |
8 |
11 |
9 CANNOT be added to LK0.thy because modal logic is built upon it, and |
12 CANNOT be added to LK0.thy because modal logic is built upon it, and |
10 various modal rules would become inconsistent. |
13 various modal rules would become inconsistent. |
11 *) |
14 *) |
12 |
15 |
14 |
17 |
15 rules |
18 rules |
16 |
19 |
17 monotonic "($H |- P ==> $H |- Q) ==> $H, P |- Q" |
20 monotonic "($H |- P ==> $H |- Q) ==> $H, P |- Q" |
18 |
21 |
|
22 left_cong "[| P == P'; |- P' ==> ($H |- $F) == ($H' |- $F') |] |
|
23 ==> (P, $H |- $F) == (P', $H' |- $F')" |
19 end |
24 end |