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