author  wenzelm 
Sun, 18 Sep 2005 15:20:08 +0200  
changeset 17481  75166ebb619b 
parent 7117  37eccadf6b8a 
child 21428  f84cf8e9cad8 
permissions  rwrr 
17481  1 
(* Title: LK/LK.ML 
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 

17481  16 
theory LK 
17 
imports LK0 

18 
uses ("simpdata.ML") 

19 
begin 

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

20 

17481  21 
axioms 
22 

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

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

24 

17481  25 
left_cong: "[ P == P';  P' ==> ($H  $F) == ($H'  $F') ] 
26 
==> (P, $H  $F) == (P', $H'  $F')" 

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

27 

17481  28 
ML {* use_legacy_bindings (the_context ()) *} 
29 

30 
use "simpdata.ML" 

31 

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

32 
end 