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 leftside formulas. Ideally it 

10 should be derived from lowerlevel 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 