author  paulson 
Mon, 06 Aug 2001 12:42:43 +0200  
changeset 11461  ffeac9aa1967 
parent 7117  37eccadf6b8a 
child 17481  75166ebb619b 
permissions  rwrr 
7094
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset

1 
(* Title: LK/LK 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

2 
ID: $Id$ 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

4 
Copyright 1993 University of Cambridge 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

5 

7094
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset

6 
Axiom to express monotonicity (a variant of the deduction theorem). Makes the 
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset

7 
link between  and ==>, needed for instance to prove imp_cong. 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

8 

7117  9 
Axiom left_cong allows the simplifier to use leftside formulas. Ideally it 
10 
should be derived from lowerlevel axioms. 

11 

7094
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset

12 
CANNOT be added to LK0.thy because modal logic is built upon it, and 
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset

13 
various modal rules would become inconsistent. 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

14 
*) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

15 

7094
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset

16 
LK = LK0 + 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

17 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

18 
rules 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

19 

7094
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset

20 
monotonic "($H  P ==> $H  Q) ==> $H, P  Q" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

21 

7117  22 
left_cong "[ P == P';  P' ==> ($H  $F) == ($H'  $F') ] 
23 
==> (P, $H  $F) == (P', $H'  $F')" 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

24 
end 