|
1 (* Title: 91/Modal/ROOT |
|
2 ID: $Id$ |
|
3 Author: Martin Coen |
|
4 Copyright 1991 University of Cambridge |
|
5 *) |
|
6 |
|
7 val banner = "Modal Logic (over LK)"; |
|
8 writeln banner; |
|
9 |
|
10 use_thy "modal0"; |
|
11 |
|
12 structure Modal0_rls = |
|
13 struct |
|
14 |
|
15 val rewrite_rls = [Modal0.strimp_def,Modal0.streqv_def]; |
|
16 |
|
17 local |
|
18 val iffR = prove_goal thy |
|
19 "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F" |
|
20 (fn prems=> |
|
21 [ (rewrite_goals_tac [iff_def]), |
|
22 (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]); |
|
23 |
|
24 val iffL = prove_goal thy |
|
25 "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E" |
|
26 (fn prems=> |
|
27 [ rewrite_goals_tac [iff_def], |
|
28 (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]) |
|
29 in |
|
30 val safe_rls = [basic,conjL,conjR,disjL,disjR,impL,impR,notL,notR,iffL,iffR]; |
|
31 val unsafe_rls = [allR,exL]; |
|
32 val bound_rls = [allL,exR]; |
|
33 end |
|
34 |
|
35 end; |
|
36 |
|
37 use "prover.ML"; |
|
38 |
|
39 use_thy"T"; |
|
40 |
|
41 local open Modal0_rls T |
|
42 in structure MP_Rule : MODAL_PROVER_RULE = |
|
43 struct |
|
44 val rewrite_rls = rewrite_rls |
|
45 val safe_rls = safe_rls |
|
46 val unsafe_rls = unsafe_rls @ [boxR,diaL] |
|
47 val bound_rls = bound_rls @ [boxL,diaR] |
|
48 val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2] |
|
49 end |
|
50 end; |
|
51 structure T_Prover = Modal_ProverFun(MP_Rule); |
|
52 |
|
53 use_thy"S4"; |
|
54 |
|
55 local open Modal0_rls S4 |
|
56 in structure MP_Rule : MODAL_PROVER_RULE = |
|
57 struct |
|
58 val rewrite_rls = rewrite_rls |
|
59 val safe_rls = safe_rls |
|
60 val unsafe_rls = unsafe_rls @ [boxR,diaL] |
|
61 val bound_rls = bound_rls @ [boxL,diaR] |
|
62 val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2] |
|
63 end; |
|
64 end; |
|
65 structure S4_Prover = Modal_ProverFun(MP_Rule); |
|
66 |
|
67 use_thy"S43"; |
|
68 |
|
69 local open Modal0_rls S43 |
|
70 in structure MP_Rule : MODAL_PROVER_RULE = |
|
71 struct |
|
72 val rewrite_rls = rewrite_rls |
|
73 val safe_rls = safe_rls |
|
74 val unsafe_rls = unsafe_rls @ [pi1,pi2] |
|
75 val bound_rls = bound_rls @ [boxL,diaR] |
|
76 val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2] |
|
77 end; |
|
78 end; |
|
79 structure S43_Prover = Modal_ProverFun(MP_Rule); |
|
80 |
|
81 val Modal_build_completed = (); (*indicate successful build*) |
|
82 |
|
83 (*printing functions are inherited from LK*) |