converted to Isar theory format;
authorwenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 1748175166ebb619b
parent 17480 fd19f77dcf60
child 17482 50e7cf6ea660
converted to Isar theory format;
src/Sequents/ILL.ML
src/Sequents/ILL.thy
src/Sequents/ILL/ILL_predlog.ML
src/Sequents/ILL/ILL_predlog.thy
src/Sequents/ILL/ROOT.ML
src/Sequents/ILL/washing.ML
src/Sequents/ILL/washing.thy
src/Sequents/LK.thy
src/Sequents/LK/Nat.ML
src/Sequents/LK/Nat.thy
src/Sequents/LK/ROOT.ML
src/Sequents/LK/hardquant.ML
src/Sequents/LK/prop.ML
src/Sequents/LK/quant.ML
src/Sequents/LK0.ML
src/Sequents/LK0.thy
src/Sequents/Modal/ROOT.ML
src/Sequents/Modal0.ML
src/Sequents/Modal0.thy
src/Sequents/ROOT.ML
src/Sequents/S4.ML
src/Sequents/S4.thy
src/Sequents/S43.ML
src/Sequents/S43.thy
src/Sequents/Sequents.thy
src/Sequents/T.ML
src/Sequents/T.thy
src/Sequents/simpdata.ML
     1.1 --- a/src/Sequents/ILL.ML	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/ILL.ML	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -2,19 +2,18 @@
     1.4      ID:         $Id$
     1.5      Author:     Sara Kalvala and Valeria de Paiva
     1.6      Copyright   1992  University of Cambridge
     1.7 -
     1.8  *)
     1.9  
    1.10  val lazy_cs = empty_pack
    1.11   add_safes [tensl, conjr, disjl, promote0,
    1.12 -	    context2,context3]
    1.13 +            context2,context3]
    1.14   add_unsafes [identity, zerol, conjll, conjlr, disjrl, disjrr,
    1.15 -	       impr, tensr, impl, derelict, weaken,
    1.16 -		 promote1, promote2,context1,context4a,context4b];
    1.17 +               impr, tensr, impl, derelict, weaken,
    1.18 +                 promote1, promote2,context1,context4a,context4b];
    1.19  
    1.20  fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n);
    1.21  
    1.22 -fun auto x = prove_goal thy x (fn prems => [best_tac lazy_cs 1]);
    1.23 +fun auto x = prove_goal (the_context ()) x (fn prems => [best_tac lazy_cs 1]);
    1.24  
    1.25  Goal "$F, $G |- A ==> $F, !(A -o B), $G |- B";
    1.26  by (rtac derelict 1);
    1.27 @@ -52,7 +51,7 @@
    1.28  by (assume_tac 1);
    1.29  qed "impr_contr_der";
    1.30  
    1.31 -val _ = goal thy "$F, (!B) -o 0, $G, !B, $H |- A";
    1.32 +val _ = goal (the_context ()) "$F, (!B) -o 0, $G, !B, $H |- A";
    1.33  by (rtac impl 1);
    1.34  by (rtac identity 3);
    1.35  by (rtac context3 1);
    1.36 @@ -61,7 +60,7 @@
    1.37  qed "contrad1";
    1.38  
    1.39  
    1.40 -val _ = goal thy "$F, !B, $G, (!B) -o 0, $H |- A";
    1.41 +val _ = goal (the_context ()) "$F, !B, $G, (!B) -o 0, $H |- A";
    1.42  by (rtac impl 1);
    1.43  by (rtac identity 3);
    1.44  by (rtac context3 1);
    1.45 @@ -69,7 +68,7 @@
    1.46  by (rtac zerol 1);
    1.47  qed "contrad2";
    1.48  
    1.49 -val _ = goal thy "A -o B, A |- B";
    1.50 +val _ = goal (the_context ()) "A -o B, A |- B";
    1.51  by (rtac impl 1);
    1.52  by (rtac identity 2);
    1.53  by (rtac identity 2);
    1.54 @@ -94,7 +93,7 @@
    1.55  by (rtac context1 1);
    1.56  qed "mp_rule2";
    1.57  
    1.58 -val _ = goal thy "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))";
    1.59 +val _ = goal (the_context ()) "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))";
    1.60  by (best_tac lazy_cs 1);
    1.61  qed "or_to_and";
    1.62  
    1.63 @@ -109,7 +108,7 @@
    1.64  
    1.65  
    1.66  
    1.67 -val _ = goal thy "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C";
    1.68 +val _ = goal (the_context ()) "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C";
    1.69  by (rtac impr 1);
    1.70  by (rtac conj_lemma 1);
    1.71  by (rtac disjl 1);
    1.72 @@ -136,20 +135,20 @@
    1.73  qed "a_not_a_rule";
    1.74  
    1.75  fun thm_to_rule x y =
    1.76 -    prove_goal thy x
    1.77 +    prove_goal (the_context ()) x
    1.78        (fn [prem] => [(rtac cut 1), (rtac y 2), (rtac prem 2),
    1.79 -	 	     (best_tac lazy_cs 1)]);
    1.80 +                     (best_tac lazy_cs 1)]);
    1.81  
    1.82  val safe_cs = lazy_cs add_safes [conj_lemma, ll_mp,contrad1,
    1.83 -				 contrad2, mp_rule1, mp_rule2, o_a_rule,
    1.84 -				 a_not_a_rule]
    1.85 -		      add_unsafes [aux_impl];
    1.86 +                                 contrad2, mp_rule1, mp_rule2, o_a_rule,
    1.87 +                                 a_not_a_rule]
    1.88 +                      add_unsafes [aux_impl];
    1.89  
    1.90  val power_cs = safe_cs add_unsafes [impr_contr_der];
    1.91  
    1.92 -fun auto1 x = prove_goal thy x (fn prems => [best_tac safe_cs 1]) ;
    1.93 +fun auto1 x = prove_goal (the_context ()) x (fn prems => [best_tac safe_cs 1]) ;
    1.94  
    1.95 -fun auto2 x = prove_goal thy x (fn prems => [best_tac power_cs 1]) ;
    1.96 +fun auto2 x = prove_goal (the_context ()) x (fn prems => [best_tac power_cs 1]) ;
    1.97  
    1.98  
    1.99  (* some examples from Troelstra and van Dalen
     2.1 --- a/src/Sequents/ILL.thy	Sun Sep 18 14:25:48 2005 +0200
     2.2 +++ b/src/Sequents/ILL.thy	Sun Sep 18 15:20:08 2005 +0200
     2.3 @@ -1,11 +1,12 @@
     2.4 -(*  Title:      ILL.thy
     2.5 +(*  Title:      Sequents/ILL.thy
     2.6      ID:         $Id$
     2.7      Author:     Sara Kalvala and Valeria de Paiva
     2.8      Copyright   1995  University of Cambridge
     2.9  *)
    2.10  
    2.11 -
    2.12 -ILL = Sequents +
    2.13 +theory ILL
    2.14 +imports Sequents
    2.15 +begin
    2.16  
    2.17  consts
    2.18    Trueprop       :: "two_seqi"
    2.19 @@ -35,98 +36,93 @@
    2.20    "@Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
    2.21    "@PromAux"  :: "three_seqe" ("promaux {_||_||_}")
    2.22  
    2.23 +parse_translation {*
    2.24 +  [("@Trueprop", single_tr "Trueprop"),
    2.25 +   ("@Context", two_seq_tr "Context"),
    2.26 +   ("@PromAux", three_seq_tr "PromAux")] *}
    2.27 +
    2.28 +print_translation {*
    2.29 +  [("Trueprop", single_tr' "@Trueprop"),
    2.30 +   ("Context", two_seq_tr'"@Context"),
    2.31 +   ("PromAux", three_seq_tr'"@PromAux")] *}
    2.32 +
    2.33  defs
    2.34  
    2.35 -liff_def        "P o-o Q == (P -o Q) >< (Q -o P)"
    2.36 +liff_def:        "P o-o Q == (P -o Q) >< (Q -o P)"
    2.37  
    2.38 -aneg_def        "~A == A -o 0"
    2.39 +aneg_def:        "~A == A -o 0"
    2.40  
    2.41  
    2.42 -
    2.43 -
    2.44 -rules
    2.45 +axioms
    2.46  
    2.47 -identity        "P |- P"
    2.48 +identity:        "P |- P"
    2.49  
    2.50 -zerol           "$G, 0, $H |- A"
    2.51 +zerol:           "$G, 0, $H |- A"
    2.52  
    2.53    (* RULES THAT DO NOT DIVIDE CONTEXT *)
    2.54  
    2.55 -derelict   "$F, A, $G |- C ==> $F, !A, $G |- C"
    2.56 +derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C"
    2.57    (* unfortunately, this one removes !A  *)
    2.58  
    2.59 -contract  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
    2.60 +contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
    2.61  
    2.62 -weaken     "$F, $G |- C ==> $G, !A, $F |- C"
    2.63 +weaken:     "$F, $G |- C ==> $G, !A, $F |- C"
    2.64    (* weak form of weakening, in practice just to clean context *)
    2.65    (* weaken and contract not needed (CHECK)  *)
    2.66  
    2.67 -promote2        "promaux{ || $H || B} ==> $H |- !B"
    2.68 -promote1        "promaux{!A, $G || $H || B}
    2.69 -                 ==> promaux {$G || $H, !A || B}"
    2.70 -promote0        "$G |- A ==> promaux {$G || || A}"
    2.71 +promote2:        "promaux{ || $H || B} ==> $H |- !B"
    2.72 +promote1:        "promaux{!A, $G || $H || B}
    2.73 +                  ==> promaux {$G || $H, !A || B}"
    2.74 +promote0:        "$G |- A ==> promaux {$G || || A}"
    2.75  
    2.76  
    2.77  
    2.78 -tensl     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
    2.79 +tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
    2.80  
    2.81 -impr      "A, $F |- B ==> $F |- A -o B"
    2.82 +impr:      "A, $F |- B ==> $F |- A -o B"
    2.83  
    2.84 -conjr           "[| $F |- A ;
    2.85 +conjr:           "[| $F |- A ;
    2.86                   $F |- B |]
    2.87                  ==> $F |- (A && B)"
    2.88  
    2.89 -conjll          "$G, A, $H |- C ==> $G, A && B, $H |- C"
    2.90 +conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C"
    2.91  
    2.92 -conjlr          "$G, B, $H |- C ==> $G, A && B, $H |- C"
    2.93 +conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C"
    2.94  
    2.95 -disjrl          "$G |- A ==> $G |- A ++ B"
    2.96 -disjrr          "$G |- B ==> $G |- A ++ B"
    2.97 -disjl           "[| $G, A, $H |- C ;
    2.98 -                    $G, B, $H |- C |]
    2.99 -                ==> $G, A ++ B, $H |- C"
   2.100 +disjrl:          "$G |- A ==> $G |- A ++ B"
   2.101 +disjrr:          "$G |- B ==> $G |- A ++ B"
   2.102 +disjl:           "[| $G, A, $H |- C ;
   2.103 +                     $G, B, $H |- C |]
   2.104 +                 ==> $G, A ++ B, $H |- C"
   2.105  
   2.106  
   2.107        (* RULES THAT DIVIDE CONTEXT *)
   2.108  
   2.109 -tensr           "[| $F, $J :=: $G;
   2.110 -                    $F |- A ;
   2.111 -                    $J |- B     |]
   2.112 -                    ==> $G |- A >< B"
   2.113 +tensr:           "[| $F, $J :=: $G;
   2.114 +                     $F |- A ;
   2.115 +                     $J |- B     |]
   2.116 +                     ==> $G |- A >< B"
   2.117  
   2.118 -impl            "[| $G, $F :=: $J, $H ;
   2.119 -                    B, $F |- C ;
   2.120 -                       $G |- A |]
   2.121 -                    ==> $J, A -o B, $H |- C"
   2.122 +impl:            "[| $G, $F :=: $J, $H ;
   2.123 +                     B, $F |- C ;
   2.124 +                        $G |- A |]
   2.125 +                     ==> $J, A -o B, $H |- C"
   2.126  
   2.127  
   2.128 -cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
   2.129 -         $H1, $H2, $H3, $H4 |- A ;
   2.130 -         $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
   2.131 +cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
   2.132 +          $H1, $H2, $H3, $H4 |- A ;
   2.133 +          $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
   2.134  
   2.135  
   2.136    (* CONTEXT RULES *)
   2.137  
   2.138 -context1     "$G :=: $G"
   2.139 -context2     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
   2.140 -context3     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
   2.141 -context4a    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
   2.142 -context4b    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
   2.143 -context5     "$F, $G :=: $H ==> $G, $F :=: $H"
   2.144 +context1:     "$G :=: $G"
   2.145 +context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
   2.146 +context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
   2.147 +context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
   2.148 +context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
   2.149 +context5:     "$F, $G :=: $H ==> $G, $F :=: $H"
   2.150  
   2.151 -
   2.152 -
   2.153 +ML {* use_legacy_bindings (the_context ()) *}
   2.154  
   2.155  end
   2.156 -
   2.157 -ML
   2.158 -
   2.159 -val parse_translation = [("@Trueprop",Sequents.single_tr "Trueprop"),
   2.160 -                         ("@Context",Sequents.two_seq_tr "Context"),
   2.161 -                         ("@PromAux", Sequents.three_seq_tr "PromAux")];
   2.162 -
   2.163 -val print_translation = [("Trueprop",Sequents.single_tr' "@Trueprop"),
   2.164 -                         ("Context",Sequents.two_seq_tr'"@Context"),
   2.165 -                         ("PromAux", Sequents.three_seq_tr'"@PromAux")];
   2.166 -
   2.167 -
     3.1 --- a/src/Sequents/ILL/ILL_predlog.ML	Sun Sep 18 14:25:48 2005 +0200
     3.2 +++ b/src/Sequents/ILL/ILL_predlog.ML	Sun Sep 18 15:20:08 2005 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  
     3.5 -fun auto1 x = prove_goal thy x
     3.6 +fun auto1 x = prove_goal (the_context ()) x
     3.7   (fn prems => [best_tac safe_cs 1]) ;
     3.8  
     3.9 -fun auto2 x = prove_goal thy x
    3.10 +fun auto2 x = prove_goal (the_context ()) x
    3.11   (fn prems => [best_tac power_cs 1]) ;
     4.1 --- a/src/Sequents/ILL/ILL_predlog.thy	Sun Sep 18 14:25:48 2005 +0200
     4.2 +++ b/src/Sequents/ILL/ILL_predlog.thy	Sun Sep 18 15:20:08 2005 +0200
     4.3 @@ -1,36 +1,32 @@
     4.4 -(* 
     4.5 -    File:	 /Nfs/toton/usr20/sk/isa_files/ll/NEW/pred_log.thy
     4.6 -    Theory Name: pred_log
     4.7 -    Logic Image: HOL
     4.8 -*)
     4.9 +(* $Id$ *)
    4.10  
    4.11 -ILL_predlog  =  ILL +
    4.12 +theory ILL_predlog
    4.13 +imports ILL
    4.14 +begin
    4.15  
    4.16 -types
    4.17 -    plf
    4.18 -    
    4.19 +typedecl plf
    4.20 +
    4.21  consts
    4.22 -
    4.23    "&"   :: "[plf,plf] => plf"   (infixr 35)
    4.24    "|"   :: "[plf,plf] => plf"   (infixr 35)
    4.25    ">"   :: "[plf,plf] => plf"   (infixr 35)
    4.26    "="   :: "[plf,plf] => plf"   (infixr 35)
    4.27    "@NG" :: "plf => plf"   ("- _ " [50] 55)
    4.28    ff    :: "plf"
    4.29 -  
    4.30 +
    4.31    PL    :: "plf => o"      ("[* / _ / *]" [] 100)
    4.32  
    4.33  
    4.34  translations
    4.35  
    4.36 -  "[* A & B *]" == "[*A*] && [*B*]" 
    4.37 +  "[* A & B *]" == "[*A*] && [*B*]"
    4.38    "[* A | B *]" == "![*A*] ++ ![*B*]"
    4.39    "[* - A *]"   == "[*A > ff*]"
    4.40    "[* ff *]"    == "0"
    4.41    "[* A = B *]" => "[* (A > B) & (B > A) *]"
    4.42 -  
    4.43 +
    4.44    "[* A > B *]" == "![*A*] -o [*B*]"
    4.45 -  
    4.46 +
    4.47  (* another translations for linear implication:
    4.48    "[* A > B *]" == "!([*A*] -o [*B*])" *)
    4.49  
     5.1 --- a/src/Sequents/ILL/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
     5.2 +++ b/src/Sequents/ILL/ROOT.ML	Sun Sep 18 15:20:08 2005 +0200
     5.3 @@ -1,3 +1,4 @@
     5.4 +(* $Id$ *)
     5.5  
     5.6  time_use_thy "washing";
     5.7  time_use_thy "ILL_predlog";
     6.1 --- a/src/Sequents/ILL/washing.ML	Sun Sep 18 14:25:48 2005 +0200
     6.2 +++ b/src/Sequents/ILL/washing.ML	Sun Sep 18 15:20:08 2005 +0200
     6.3 @@ -1,3 +1,5 @@
     6.4 +(* $Id$ *)
     6.5 +
     6.6  (* "activate" definitions for use in proof *)
     6.7  
     6.8  val changeI = [context1] RL ([change] RLN (2,[cut]));
     6.9 @@ -16,15 +18,11 @@
    6.10  
    6.11  (* order of premises doesn't matter *)
    6.12  
    6.13 -prove_goal thy "dollar , dirty , dollar |- clean"
    6.14 +prove_goal (the_context ()) "dollar , dirty , dollar |- clean"
    6.15  (fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
    6.16  
    6.17  
    6.18  (* alternative formulation *)
    6.19  
    6.20 -prove_goal thy "dollar , dollar |- dirty -o clean"
    6.21 +prove_goal (the_context ()) "dollar , dollar |- dirty -o clean"
    6.22  (fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
    6.23 -
    6.24 -
    6.25 -
    6.26 -
     7.1 --- a/src/Sequents/ILL/washing.thy	Sun Sep 18 14:25:48 2005 +0200
     7.2 +++ b/src/Sequents/ILL/washing.thy	Sun Sep 18 15:20:08 2005 +0200
     7.3 @@ -1,33 +1,38 @@
     7.4 -
     7.5  
     7.6 -(* code by Sara Kalvala, based on Paulson's LK 
     7.7 +(* $Id$ *)
     7.8 +
     7.9 +(* code by Sara Kalvala, based on Paulson's LK
    7.10                             and Moore's tisl.ML *)
    7.11  
    7.12 -washing = ILL +
    7.13 +theory washing
    7.14 +imports ILL
    7.15 +begin
    7.16  
    7.17  consts
    7.18 -
    7.19 -dollar,quarter,loaded,dirty,wet,clean        :: "o"			
    7.20 +  dollar :: o
    7.21 +  quarter :: o
    7.22 +  loaded :: o
    7.23 +  dirty :: o
    7.24 +  wet :: o
    7.25 +  clean :: o
    7.26  
    7.27 -  
    7.28 -rules
    7.29 -
    7.30 -
    7.31 -  change
    7.32 +axioms
    7.33 +  change:
    7.34    "dollar |- (quarter >< quarter >< quarter >< quarter)"
    7.35  
    7.36 -  load1
    7.37 +  load1:
    7.38    "quarter , quarter , quarter , quarter , quarter |- loaded"
    7.39  
    7.40 -  load2
    7.41 +  load2:
    7.42    "dollar , quarter |- loaded"
    7.43  
    7.44 -  wash
    7.45 +  wash:
    7.46    "loaded , dirty |- wet"
    7.47  
    7.48 -  dry
    7.49 +  dry:
    7.50    "wet, quarter , quarter , quarter |- clean"
    7.51  
    7.52 +ML {* use_legacy_bindings (the_context ()) *}
    7.53 +
    7.54  end
    7.55  
    7.56 -  
    7.57 \ No newline at end of file
     8.1 --- a/src/Sequents/LK.thy	Sun Sep 18 14:25:48 2005 +0200
     8.2 +++ b/src/Sequents/LK.thy	Sun Sep 18 15:20:08 2005 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      LK/LK
     8.5 +(*  Title:      LK/LK.ML
     8.6      ID:         $Id$
     8.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.8      Copyright   1993  University of Cambridge
     8.9 @@ -13,12 +13,20 @@
    8.10  various modal rules would become inconsistent.
    8.11  *)
    8.12  
    8.13 -LK = LK0 +
    8.14 +theory LK
    8.15 +imports LK0
    8.16 +uses ("simpdata.ML")
    8.17 +begin
    8.18  
    8.19 -rules
    8.20 +axioms
    8.21 +
    8.22 +  monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
    8.23  
    8.24 -  monotonic  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
    8.25 +  left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
    8.26 +               ==> (P, $H |- $F) == (P', $H' |- $F')"
    8.27  
    8.28 -  left_cong  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |] 
    8.29 -              ==> (P, $H |- $F) == (P', $H' |- $F')"
    8.30 +ML {* use_legacy_bindings (the_context ()) *}
    8.31 +
    8.32 +use "simpdata.ML"
    8.33 +
    8.34  end
     9.1 --- a/src/Sequents/LK/Nat.ML	Sun Sep 18 14:25:48 2005 +0200
     9.2 +++ b/src/Sequents/LK/Nat.ML	Sun Sep 18 15:20:08 2005 +0200
     9.3 @@ -1,9 +1,7 @@
     9.4 -(*  Title:      Sequents/LK/Nat
     9.5 +(*  Title:      Sequents/LK/Nat.ML
     9.6      ID:         $Id$
     9.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.8      Copyright   1999  University of Cambridge
     9.9 -
    9.10 -Theory of the natural numbers: Peano's axioms, primitive recursion
    9.11  *)
    9.12  
    9.13  Addsimps [Suc_neq_0];
    10.1 --- a/src/Sequents/LK/Nat.thy	Sun Sep 18 14:25:48 2005 +0200
    10.2 +++ b/src/Sequents/LK/Nat.thy	Sun Sep 18 15:20:08 2005 +0200
    10.3 @@ -1,26 +1,32 @@
    10.4 -(*  Title:      Sequents/LK/Nat
    10.5 +(*  Title:      Sequents/LK/Nat.thy
    10.6      ID:         $Id$
    10.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.8      Copyright   1999  University of Cambridge
    10.9 -
   10.10 -Theory of the natural numbers: Peano's axioms, primitive recursion
   10.11  *)
   10.12  
   10.13 -Nat = LK +
   10.14 -types   nat
   10.15 -arities nat :: term
   10.16 +header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
   10.17 +
   10.18 +theory Nat
   10.19 +imports LK
   10.20 +begin
   10.21 +
   10.22 +typedecl nat
   10.23 +arities nat :: "term"
   10.24  consts  "0" :: nat      ("0")
   10.25 -        Suc :: nat=>nat  
   10.26 -        rec :: [nat, 'a, [nat,'a]=>'a] => 'a  
   10.27 -        "+" :: [nat, nat] => nat                (infixl 60)
   10.28 +        Suc :: "nat=>nat"
   10.29 +        rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
   10.30 +        "+" :: "[nat, nat] => nat"                (infixl 60)
   10.31  
   10.32 -rules   
   10.33 -  induct  "[| $H |- $E, P(0), $F;
   10.34 +axioms
   10.35 +  induct:  "[| $H |- $E, P(0), $F;
   10.36                !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
   10.37  
   10.38 -  Suc_inject  "|- Suc(m)=Suc(n) --> m=n"
   10.39 -  Suc_neq_0   "|- Suc(m) ~= 0"
   10.40 -  rec_0       "|- rec(0,a,f) = a"
   10.41 -  rec_Suc     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
   10.42 -  add_def     "m+n == rec(m, n, %x y. Suc(y))"
   10.43 +  Suc_inject:  "|- Suc(m)=Suc(n) --> m=n"
   10.44 +  Suc_neq_0:   "|- Suc(m) ~= 0"
   10.45 +  rec_0:       "|- rec(0,a,f) = a"
   10.46 +  rec_Suc:     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
   10.47 +  add_def:     "m+n == rec(m, n, %x y. Suc(y))"
   10.48 +
   10.49 +ML {* use_legacy_bindings (the_context ()) *}
   10.50 +
   10.51  end
    11.1 --- a/src/Sequents/LK/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
    11.2 +++ b/src/Sequents/LK/ROOT.ML	Sun Sep 18 15:20:08 2005 +0200
    11.3 @@ -3,7 +3,7 @@
    11.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.5      Copyright   1992  University of Cambridge
    11.6  
    11.7 -Executes all examples for Classical Logic. 
    11.8 +Examples for Classical Logic.
    11.9  *)
   11.10  
   11.11  time_use "prop.ML";
    12.1 --- a/src/Sequents/LK/hardquant.ML	Sun Sep 18 14:25:48 2005 +0200
    12.2 +++ b/src/Sequents/LK/hardquant.ML	Sun Sep 18 15:20:08 2005 +0200
    12.3 @@ -12,25 +12,23 @@
    12.4  Uses pc_tac rather than fast_tac when the former is significantly faster.
    12.5  *)
    12.6  
    12.7 -writeln"File LK/ex/hard-quant.";
    12.8 -
    12.9 -context LK.thy;
   12.10 +context (theory "LK");
   12.11  
   12.12  Goal "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
   12.13  by (Fast_tac 1);
   12.14 -result(); 
   12.15 +result();
   12.16  
   12.17  Goal "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
   12.18  by (Fast_tac 1);
   12.19 -result(); 
   12.20 +result();
   12.21  
   12.22  Goal "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
   12.23  by (Fast_tac 1);
   12.24 -result(); 
   12.25 +result();
   12.26  
   12.27  Goal "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
   12.28  by (Fast_tac 1);
   12.29 -result(); 
   12.30 +result();
   12.31  
   12.32  writeln"Problems requiring quantifier duplication";
   12.33  
   12.34 @@ -53,7 +51,7 @@
   12.35  writeln"Problem 18";
   12.36  Goal "|- EX y. ALL x. P(y)-->P(x)";
   12.37  by (best_tac LK_dup_pack 1);
   12.38 -result(); 
   12.39 +result();
   12.40  
   12.41  writeln"Problem 19";
   12.42  Goal "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
   12.43 @@ -63,7 +61,7 @@
   12.44  writeln"Problem 20";
   12.45  Goal "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
   12.46  \   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
   12.47 -by (Fast_tac 1); 
   12.48 +by (Fast_tac 1);
   12.49  result();
   12.50  
   12.51  writeln"Problem 21";
   12.52 @@ -73,12 +71,12 @@
   12.53  
   12.54  writeln"Problem 22";
   12.55  Goal "|- (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
   12.56 -by (Fast_tac 1); 
   12.57 +by (Fast_tac 1);
   12.58  result();
   12.59  
   12.60  writeln"Problem 23";
   12.61  Goal "|- (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
   12.62 -by (best_tac LK_pack 1);  
   12.63 +by (best_tac LK_pack 1);
   12.64  result();
   12.65  
   12.66  writeln"Problem 24";
   12.67 @@ -94,7 +92,7 @@
   12.68  \       (ALL x. P(x) --> (M(x) & L(x))) &   \
   12.69  \       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
   12.70  \   --> (EX x. Q(x)&P(x))";
   12.71 -by (best_tac LK_pack 1);  
   12.72 +by (best_tac LK_pack 1);
   12.73  result();
   12.74  
   12.75  writeln"Problem 26";
   12.76 @@ -110,7 +108,7 @@
   12.77  \             (ALL x. M(x) & L(x) --> P(x)) &   \
   12.78  \             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
   12.79  \         --> (ALL x. M(x) --> ~L(x))";
   12.80 -by (pc_tac LK_pack 1); 
   12.81 +by (pc_tac LK_pack 1);
   12.82  result();
   12.83  
   12.84  writeln"Problem 28.  AMENDED";
   12.85 @@ -118,21 +116,21 @@
   12.86  \       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
   12.87  \       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
   12.88  \   --> (ALL x. P(x) & L(x) --> M(x))";
   12.89 -by (pc_tac LK_pack 1);  
   12.90 +by (pc_tac LK_pack 1);
   12.91  result();
   12.92  
   12.93  writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
   12.94  Goal "|- (EX x. P(x)) & (EX y. Q(y))  \
   12.95  \   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
   12.96  \        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
   12.97 -by (pc_tac LK_pack 1); 
   12.98 +by (pc_tac LK_pack 1);
   12.99  result();
  12.100  
  12.101  writeln"Problem 30";
  12.102  Goal "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & \
  12.103  \       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
  12.104  \   --> (ALL x. S(x))";
  12.105 -by (Fast_tac 1);  
  12.106 +by (Fast_tac 1);
  12.107  result();
  12.108  
  12.109  writeln"Problem 31";
  12.110 @@ -238,7 +236,7 @@
  12.111  \     (EX x. f(x) & (ALL y. h(x,y) --> l(y))                    \
  12.112  \                  & (ALL y. g(y) & h(x,y) --> j(x,y)))         \
  12.113  \     --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
  12.114 -by (best_tac LK_pack 1); 
  12.115 +by (best_tac LK_pack 1);
  12.116  result();
  12.117  
  12.118  
  12.119 @@ -249,7 +247,7 @@
  12.120  by (fast_tac (pack() add_safes [subst]) 1);
  12.121  result();
  12.122  
  12.123 -writeln"Problem 50";  
  12.124 +writeln"Problem 50";
  12.125  Goal "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
  12.126  by (best_tac LK_dup_pack 1);
  12.127  result();
  12.128 @@ -287,7 +285,7 @@
  12.129  writeln"Problem 59";
  12.130  (*Unification works poorly here -- the abstraction %sobj prevents efficient
  12.131    operation of the occurs check*)
  12.132 -Unify.trace_bound := !Unify.search_bound - 1; 
  12.133 +Unify.trace_bound := !Unify.search_bound - 1;
  12.134  Goal "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
  12.135  by (best_tac LK_dup_pack 1);
  12.136  result();
  12.137 @@ -304,8 +302,7 @@
  12.138  by (Fast_tac 1);
  12.139  result();
  12.140  
  12.141 -writeln"Reached end of file.";
  12.142 -
  12.143  (*18 June 92: loaded in 372 secs*)
  12.144  (*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
  12.145  (*29 June 92: loaded in 370 secs*)
  12.146 +(*18 September 2005: loaded in 1.809 secs*)
    13.1 --- a/src/Sequents/LK/prop.ML	Sun Sep 18 14:25:48 2005 +0200
    13.2 +++ b/src/Sequents/LK/prop.ML	Sun Sep 18 15:20:08 2005 +0200
    13.3 @@ -7,93 +7,91 @@
    13.4  Can be read to test the LK system.
    13.5  *)
    13.6  
    13.7 -writeln"LK/ex/prop: propositional examples";
    13.8 -
    13.9  writeln"absorptive laws of & and | ";
   13.10  
   13.11 -goal LK.thy "|- P & P <-> P";
   13.12 +goal (theory "LK") "|- P & P <-> P";
   13.13  by (fast_tac prop_pack 1);
   13.14  result();
   13.15  
   13.16 -goal LK.thy "|- P | P <-> P";
   13.17 +goal (theory "LK") "|- P | P <-> P";
   13.18  by (fast_tac prop_pack 1);
   13.19  result();
   13.20  
   13.21  writeln"commutative laws of & and | ";
   13.22  
   13.23 -goal LK.thy "|- P & Q  <->  Q & P";
   13.24 +goal (theory "LK") "|- P & Q  <->  Q & P";
   13.25  by (fast_tac prop_pack 1);
   13.26  result();
   13.27  
   13.28 -goal LK.thy "|- P | Q  <->  Q | P";
   13.29 +goal (theory "LK") "|- P | Q  <->  Q | P";
   13.30  by (fast_tac prop_pack 1);
   13.31  result();
   13.32  
   13.33  
   13.34  writeln"associative laws of & and | ";
   13.35  
   13.36 -goal LK.thy "|- (P & Q) & R  <->  P & (Q & R)";
   13.37 +goal (theory "LK") "|- (P & Q) & R  <->  P & (Q & R)";
   13.38  by (fast_tac prop_pack 1);
   13.39  result();
   13.40  
   13.41 -goal LK.thy "|- (P | Q) | R  <->  P | (Q | R)";
   13.42 +goal (theory "LK") "|- (P | Q) | R  <->  P | (Q | R)";
   13.43  by (fast_tac prop_pack 1);
   13.44  result();
   13.45  
   13.46  writeln"distributive laws of & and | ";
   13.47 -goal LK.thy "|- (P & Q) | R  <-> (P | R) & (Q | R)";
   13.48 +goal (theory "LK") "|- (P & Q) | R  <-> (P | R) & (Q | R)";
   13.49  by (fast_tac prop_pack 1);
   13.50  result();
   13.51  
   13.52 -goal LK.thy "|- (P | Q) & R  <-> (P & R) | (Q & R)";
   13.53 +goal (theory "LK") "|- (P | Q) & R  <-> (P & R) | (Q & R)";
   13.54  by (fast_tac prop_pack 1);
   13.55  result();
   13.56  
   13.57  writeln"Laws involving implication";
   13.58  
   13.59 -goal LK.thy "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
   13.60 +goal (theory "LK") "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
   13.61  by (fast_tac prop_pack 1);
   13.62  result(); 
   13.63  
   13.64 -goal LK.thy "|- (P & Q --> R) <-> (P--> (Q-->R))";
   13.65 +goal (theory "LK") "|- (P & Q --> R) <-> (P--> (Q-->R))";
   13.66  by (fast_tac prop_pack 1);
   13.67  result(); 
   13.68  
   13.69  
   13.70 -goal LK.thy "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
   13.71 +goal (theory "LK") "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
   13.72  by (fast_tac prop_pack 1);
   13.73  result();
   13.74  
   13.75  
   13.76  writeln"Classical theorems";
   13.77  
   13.78 -goal LK.thy "|- P|Q --> P| ~P&Q";
   13.79 +goal (theory "LK") "|- P|Q --> P| ~P&Q";
   13.80  by (fast_tac prop_pack 1);
   13.81  result();
   13.82  
   13.83  
   13.84 -goal LK.thy "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
   13.85 +goal (theory "LK") "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
   13.86  by (fast_tac prop_pack 1);
   13.87  result();
   13.88  
   13.89  
   13.90 -goal LK.thy "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
   13.91 +goal (theory "LK") "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
   13.92  by (fast_tac prop_pack 1);
   13.93  result();
   13.94  
   13.95  
   13.96 -goal LK.thy "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
   13.97 +goal (theory "LK") "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
   13.98  by (fast_tac prop_pack 1);
   13.99  result();
  13.100  
  13.101  
  13.102  (*If and only if*)
  13.103  
  13.104 -goal LK.thy "|- (P<->Q) <-> (Q<->P)";
  13.105 +goal (theory "LK") "|- (P<->Q) <-> (Q<->P)";
  13.106  by (fast_tac prop_pack 1);
  13.107  result();
  13.108  
  13.109 -goal LK.thy "|- ~ (P <-> ~P)";
  13.110 +goal (theory "LK") "|- ~ (P <-> ~P)";
  13.111  by (fast_tac prop_pack 1);
  13.112  result();
  13.113  
  13.114 @@ -106,89 +104,87 @@
  13.115  *)
  13.116  
  13.117  (*1*)
  13.118 -goal LK.thy "|- (P-->Q)  <->  (~Q --> ~P)";
  13.119 +goal (theory "LK") "|- (P-->Q)  <->  (~Q --> ~P)";
  13.120  by (fast_tac prop_pack 1);
  13.121  result();
  13.122  
  13.123  (*2*)
  13.124 -goal LK.thy "|- ~ ~ P  <->  P";
  13.125 +goal (theory "LK") "|- ~ ~ P  <->  P";
  13.126  by (fast_tac prop_pack 1);
  13.127  result();
  13.128  
  13.129  (*3*)
  13.130 -goal LK.thy "|- ~(P-->Q) --> (Q-->P)";
  13.131 +goal (theory "LK") "|- ~(P-->Q) --> (Q-->P)";
  13.132  by (fast_tac prop_pack 1);
  13.133  result();
  13.134  
  13.135  (*4*)
  13.136 -goal LK.thy "|- (~P-->Q)  <->  (~Q --> P)";
  13.137 +goal (theory "LK") "|- (~P-->Q)  <->  (~Q --> P)";
  13.138  by (fast_tac prop_pack 1);
  13.139  result();
  13.140  
  13.141  (*5*)
  13.142 -goal LK.thy "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
  13.143 +goal (theory "LK") "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
  13.144  by (fast_tac prop_pack 1);
  13.145  result();
  13.146  
  13.147  (*6*)
  13.148 -goal LK.thy "|- P | ~ P";
  13.149 +goal (theory "LK") "|- P | ~ P";
  13.150  by (fast_tac prop_pack 1);
  13.151  result();
  13.152  
  13.153  (*7*)
  13.154 -goal LK.thy "|- P | ~ ~ ~ P";
  13.155 +goal (theory "LK") "|- P | ~ ~ ~ P";
  13.156  by (fast_tac prop_pack 1);
  13.157  result();
  13.158  
  13.159  (*8.  Peirce's law*)
  13.160 -goal LK.thy "|- ((P-->Q) --> P)  -->  P";
  13.161 +goal (theory "LK") "|- ((P-->Q) --> P)  -->  P";
  13.162  by (fast_tac prop_pack 1);
  13.163  result();
  13.164  
  13.165  (*9*)
  13.166 -goal LK.thy "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
  13.167 +goal (theory "LK") "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
  13.168  by (fast_tac prop_pack 1);
  13.169  result();
  13.170  
  13.171  (*10*)
  13.172 -goal LK.thy "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
  13.173 +goal (theory "LK") "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
  13.174  by (fast_tac prop_pack 1);
  13.175  result();
  13.176  
  13.177  (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
  13.178 -goal LK.thy "|- P<->P";
  13.179 +goal (theory "LK") "|- P<->P";
  13.180  by (fast_tac prop_pack 1);
  13.181  result();
  13.182  
  13.183  (*12.  "Dijkstra's law"*)
  13.184 -goal LK.thy "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
  13.185 +goal (theory "LK") "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
  13.186  by (fast_tac prop_pack 1);
  13.187  result();
  13.188  
  13.189  (*13.  Distributive law*)
  13.190 -goal LK.thy "|- P | (Q & R)  <-> (P | Q) & (P | R)";
  13.191 +goal (theory "LK") "|- P | (Q & R)  <-> (P | Q) & (P | R)";
  13.192  by (fast_tac prop_pack 1);
  13.193  result();
  13.194  
  13.195  (*14*)
  13.196 -goal LK.thy "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
  13.197 +goal (theory "LK") "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
  13.198  by (fast_tac prop_pack 1);
  13.199  result();
  13.200  
  13.201  
  13.202  (*15*)
  13.203 -goal LK.thy "|- (P --> Q) <-> (~P | Q)";
  13.204 +goal (theory "LK") "|- (P --> Q) <-> (~P | Q)";
  13.205  by (fast_tac prop_pack 1);
  13.206  result();
  13.207  
  13.208  (*16*)
  13.209 -goal LK.thy "|- (P-->Q) | (Q-->P)";
  13.210 +goal (theory "LK") "|- (P-->Q) | (Q-->P)";
  13.211  by (fast_tac prop_pack 1);
  13.212  result();
  13.213  
  13.214  (*17*)
  13.215 -goal LK.thy "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
  13.216 +goal (theory "LK") "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
  13.217  by (fast_tac prop_pack 1);
  13.218  result();
  13.219 -
  13.220 -writeln"Reached end of file.";
    14.1 --- a/src/Sequents/LK/quant.ML	Sun Sep 18 14:25:48 2005 +0200
    14.2 +++ b/src/Sequents/LK/quant.ML	Sun Sep 18 15:20:08 2005 +0200
    14.3 @@ -1,4 +1,4 @@
    14.4 -(*  Title:      LK/ex/quant
    14.5 +(*  Title:      LK/ex/quant.ML
    14.6      ID:         $Id$
    14.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.8      Copyright   1992  University of Cambridge
    14.9 @@ -6,155 +6,151 @@
   14.10  Classical sequent calculus: examples with quantifiers.
   14.11  *)
   14.12  
   14.13 -
   14.14 -writeln"LK/ex/quant: Examples with quantifiers";
   14.15 -
   14.16 -goal LK.thy "|- (ALL x. P)  <->  P";
   14.17 +goal (theory "LK") "|- (ALL x. P)  <->  P";
   14.18  by (fast_tac LK_pack 1);
   14.19 -result(); 
   14.20 +result();
   14.21  
   14.22 -goal LK.thy "|- (ALL x y. P(x,y))  <->  (ALL y x. P(x,y))";
   14.23 +goal (theory "LK") "|- (ALL x y. P(x,y))  <->  (ALL y x. P(x,y))";
   14.24  by (fast_tac LK_pack 1);
   14.25 -result(); 
   14.26 +result();
   14.27  
   14.28 -goal LK.thy "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)";
   14.29 +goal (theory "LK") "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)";
   14.30  by (fast_tac LK_pack 1);
   14.31 -result(); 
   14.32 +result();
   14.33  
   14.34  writeln"Permutation of existential quantifier.";
   14.35 -goal LK.thy "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))";
   14.36 +goal (theory "LK") "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))";
   14.37  by (fast_tac LK_pack 1);
   14.38 -result(); 
   14.39 +result();
   14.40  
   14.41 -goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
   14.42 +goal (theory "LK") "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
   14.43  by (fast_tac LK_pack 1);
   14.44 -result(); 
   14.45 +result();
   14.46  
   14.47  
   14.48  (*Converse is invalid*)
   14.49 -goal LK.thy "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))";
   14.50 +goal (theory "LK") "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))";
   14.51  by (fast_tac LK_pack 1);
   14.52 -result(); 
   14.53 +result();
   14.54  
   14.55  
   14.56  writeln"Pushing ALL into an implication.";
   14.57 -goal LK.thy "|- (ALL x. P --> Q(x))  <->  (P --> (ALL x. Q(x)))";
   14.58 +goal (theory "LK") "|- (ALL x. P --> Q(x))  <->  (P --> (ALL x. Q(x)))";
   14.59  by (fast_tac LK_pack 1);
   14.60 -result(); 
   14.61 +result();
   14.62  
   14.63  
   14.64 -goal LK.thy "|- (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
   14.65 +goal (theory "LK") "|- (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
   14.66  by (fast_tac LK_pack 1);
   14.67 -result(); 
   14.68 +result();
   14.69  
   14.70  
   14.71 -goal LK.thy "|- (EX x. P)  <->  P";
   14.72 +goal (theory "LK") "|- (EX x. P)  <->  P";
   14.73  by (fast_tac LK_pack 1);
   14.74 -result(); 
   14.75 +result();
   14.76  
   14.77  
   14.78  writeln"Distribution of EX over disjunction.";
   14.79 -goal LK.thy "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x))  |  (EX x. Q(x))";
   14.80 +goal (theory "LK") "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x))  |  (EX x. Q(x))";
   14.81  by (fast_tac LK_pack 1);
   14.82 -result(); 
   14.83 +result();
   14.84  (*5 secs*)
   14.85  
   14.86  (*Converse is invalid*)
   14.87 -goal LK.thy "|- (EX x. P(x) & Q(x))  -->  (EX x. P(x))  &  (EX x. Q(x))";
   14.88 +goal (theory "LK") "|- (EX x. P(x) & Q(x))  -->  (EX x. P(x))  &  (EX x. Q(x))";
   14.89  by (fast_tac LK_pack 1);
   14.90 -result(); 
   14.91 +result();
   14.92  
   14.93  
   14.94  writeln"Harder examples: classical theorems.";
   14.95  
   14.96 -goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
   14.97 +goal (theory "LK") "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
   14.98  by (fast_tac LK_pack 1);
   14.99 -result(); 
  14.100 +result();
  14.101  (*3 secs*)
  14.102  
  14.103  
  14.104 -goal LK.thy "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
  14.105 +goal (theory "LK") "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
  14.106  by (fast_tac LK_pack 1);
  14.107 -result(); 
  14.108 +result();
  14.109  (*5 secs*)
  14.110  
  14.111  
  14.112 -goal LK.thy "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
  14.113 +goal (theory "LK") "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
  14.114  by (fast_tac LK_pack 1);
  14.115 -result(); 
  14.116 +result();
  14.117  
  14.118  
  14.119  writeln"Basic test of quantifier reasoning";
  14.120 -goal LK.thy
  14.121 +goal (theory "LK")
  14.122     "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
  14.123  by (fast_tac LK_pack 1);
  14.124 -result();  
  14.125 +result();
  14.126  
  14.127  
  14.128 -goal LK.thy "|- (ALL x. Q(x))  -->  (EX x. Q(x))";
  14.129 +goal (theory "LK") "|- (ALL x. Q(x))  -->  (EX x. Q(x))";
  14.130  by (fast_tac LK_pack 1);
  14.131 -result();  
  14.132 +result();
  14.133  
  14.134  
  14.135  writeln"The following are invalid!";
  14.136  
  14.137  (*INVALID*)
  14.138 -goal LK.thy "|- (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
  14.139 -by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; 
  14.140 +goal (theory "LK") "|- (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
  14.141 +by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  14.142  (*Check that subgoals remain: proof failed.*)
  14.143 -getgoal 1; 
  14.144 +getgoal 1;
  14.145  
  14.146  (*INVALID*)
  14.147 -goal LK.thy "|- (EX x. Q(x))  -->  (ALL x. Q(x))";
  14.148 +goal (theory "LK") "|- (EX x. Q(x))  -->  (ALL x. Q(x))";
  14.149  by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  14.150 -getgoal 1; 
  14.151 +getgoal 1;
  14.152  
  14.153 -goal LK.thy "|- P(?a) --> (ALL x. P(x))";
  14.154 +goal (theory "LK") "|- P(?a) --> (ALL x. P(x))";
  14.155  by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  14.156  (*Check that subgoals remain: proof failed.*)
  14.157 -getgoal 1;  
  14.158 +getgoal 1;
  14.159  
  14.160 -goal LK.thy "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
  14.161 +goal (theory "LK") "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
  14.162  by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
  14.163 -getgoal 1;  
  14.164 +getgoal 1;
  14.165  
  14.166  
  14.167  writeln"Back to things that are provable...";
  14.168  
  14.169 -goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
  14.170 -by (fast_tac LK_pack 1); 
  14.171 -result();  
  14.172 +goal (theory "LK") "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
  14.173 +by (fast_tac LK_pack 1);
  14.174 +result();
  14.175  
  14.176  (*An example of why exR should be delayed as long as possible*)
  14.177 -goal LK.thy "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))";
  14.178 +goal (theory "LK") "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))";
  14.179  by (fast_tac LK_pack 1);
  14.180 -result();  
  14.181 +result();
  14.182  
  14.183  writeln"Solving for a Var";
  14.184 -goal LK.thy 
  14.185 +goal (theory "LK")
  14.186     "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
  14.187  by (fast_tac LK_pack 1);
  14.188  result();
  14.189  
  14.190  
  14.191  writeln"Principia Mathematica *11.53";
  14.192 -goal LK.thy 
  14.193 +goal (theory "LK")
  14.194      "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
  14.195  by (fast_tac LK_pack 1);
  14.196  result();
  14.197  
  14.198  
  14.199  writeln"Principia Mathematica *11.55";
  14.200 -goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
  14.201 +goal (theory "LK") "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
  14.202  by (fast_tac LK_pack 1);
  14.203  result();
  14.204  
  14.205  writeln"Principia Mathematica *11.61";
  14.206 -goal LK.thy
  14.207 +goal (theory "LK")
  14.208     "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
  14.209  by (fast_tac LK_pack 1);
  14.210  result();
  14.211  
  14.212 -writeln"Reached end of file.";
  14.213 -
  14.214  (*21 August 88: loaded in 45.7 secs*)
  14.215 +(*18 September 2005: loaded in 0.114 secs*)
    15.1 --- a/src/Sequents/LK0.ML	Sun Sep 18 14:25:48 2005 +0200
    15.2 +++ b/src/Sequents/LK0.ML	Sun Sep 18 15:20:08 2005 +0200
    15.3 @@ -1,9 +1,9 @@
    15.4 -(*  Title:      LK/LK0
    15.5 +(*  Title:      LK/LK0.ML
    15.6      ID:         $Id$
    15.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.8      Copyright   1992  University of Cambridge
    15.9  
   15.10 -Tactics and lemmas for LK (thanks also to Philippe de Groote)  
   15.11 +Tactics and lemmas for LK (thanks also to Philippe de Groote)
   15.12  
   15.13  Structural rules by Soren Heilmann
   15.14  *)
   15.15 @@ -41,21 +41,21 @@
   15.16  qed "exchL";
   15.17  
   15.18  (*Cut and thin, replacing the right-side formula*)
   15.19 -fun cutR_tac (sP: string) i = 
   15.20 +fun cutR_tac (sP: string) i =
   15.21      res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
   15.22  
   15.23  (*Cut and thin, replacing the left-side formula*)
   15.24 -fun cutL_tac (sP: string) i = 
   15.25 +fun cutL_tac (sP: string) i =
   15.26      res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);
   15.27  
   15.28  
   15.29  (** If-and-only-if rules **)
   15.30 -Goalw [iff_def] 
   15.31 +Goalw [iff_def]
   15.32      "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F";
   15.33  by (REPEAT (ares_tac [conjR,impR] 1));
   15.34  qed "iffR";
   15.35  
   15.36 -Goalw [iff_def] 
   15.37 +Goalw [iff_def]
   15.38      "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E";
   15.39  by (REPEAT (ares_tac [conjL,impL,basic] 1));
   15.40  qed "iffL";
   15.41 @@ -93,31 +93,31 @@
   15.42  
   15.43  
   15.44  (*The rules of LK*)
   15.45 -val prop_pack = empty_pack add_safes 
   15.46 -                [basic, refl, TrueR, FalseL, 
   15.47 -		 conjL, conjR, disjL, disjR, impL, impR, 
   15.48 +val prop_pack = empty_pack add_safes
   15.49 +                [basic, refl, TrueR, FalseL,
   15.50 +                 conjL, conjR, disjL, disjR, impL, impR,
   15.51                   notL, notR, iffL, iffR];
   15.52  
   15.53 -val LK_pack = prop_pack add_safes   [allR, exL] 
   15.54 +val LK_pack = prop_pack add_safes   [allR, exL]
   15.55                          add_unsafes [allL_thin, exR_thin, the_equality];
   15.56  
   15.57 -val LK_dup_pack = prop_pack add_safes   [allR, exL] 
   15.58 +val LK_dup_pack = prop_pack add_safes   [allR, exL]
   15.59                              add_unsafes [allL, exR, the_equality];
   15.60  
   15.61  
   15.62  pack_ref() := LK_pack;
   15.63  
   15.64 -fun lemma_tac th i = 
   15.65 +fun lemma_tac th i =
   15.66      rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
   15.67  
   15.68 -val [major,minor] = goal thy 
   15.69 +val [major,minor] = goal (the_context ())
   15.70      "[| $H |- $E, $F, P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
   15.71  by (rtac (thinRS RS cut) 1 THEN rtac major 1);
   15.72  by (Step_tac 1);
   15.73  by (rtac thinR 1 THEN rtac minor 1);
   15.74  qed "mp_R";
   15.75  
   15.76 -val [major,minor] = goal thy 
   15.77 +val [major,minor] = goal (the_context ())
   15.78      "[| $H, $G |- $E, P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
   15.79  by (rtac (thinL RS cut) 1 THEN rtac major 1);
   15.80  by (Step_tac 1);
   15.81 @@ -127,14 +127,14 @@
   15.82  
   15.83  (** Two rules to generate left- and right- rules from implications **)
   15.84  
   15.85 -val [major,minor] = goal thy 
   15.86 +val [major,minor] = goal (the_context ())
   15.87      "[| |- P --> Q;  $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
   15.88  by (rtac mp_R 1);
   15.89  by (rtac minor 2);
   15.90  by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
   15.91  qed "R_of_imp";
   15.92  
   15.93 -val [major,minor] = goal thy 
   15.94 +val [major,minor] = goal (the_context ())
   15.95      "[| |- P --> Q;  $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
   15.96  by (rtac mp_L 1);
   15.97  by (rtac minor 2);
   15.98 @@ -142,7 +142,7 @@
   15.99  qed "L_of_imp";
  15.100  
  15.101  (*Can be used to create implications in a subgoal*)
  15.102 -val [prem] = goal thy 
  15.103 +val [prem] = goal (the_context ())
  15.104      "[| $H, $G |- $E, $F, P --> Q |] ==> $H, P, $G |- $E, Q, $F";
  15.105  by (rtac mp_L 1);
  15.106  by (rtac basic 2);
  15.107 @@ -151,17 +151,17 @@
  15.108  
  15.109  Goal "|-P&Q ==> |-P";
  15.110  by (etac (thinR RS cut) 1);
  15.111 -by (Fast_tac 1);		
  15.112 +by (Fast_tac 1);
  15.113  qed "conjunct1";
  15.114  
  15.115  Goal "|-P&Q ==> |-Q";
  15.116  by (etac (thinR RS cut) 1);
  15.117 -by (Fast_tac 1);		
  15.118 +by (Fast_tac 1);
  15.119  qed "conjunct2";
  15.120  
  15.121  Goal "|- (ALL x. P(x)) ==> |- P(x)";
  15.122  by (etac (thinR RS cut) 1);
  15.123 -by (Fast_tac 1);		
  15.124 +by (Fast_tac 1);
  15.125  qed "spec";
  15.126  
  15.127  (** Equality **)
  15.128 @@ -189,12 +189,12 @@
  15.129  (* Two theorms for rewriting only one instance of a definition:
  15.130     the first for definitions of formulae and the second for terms *)
  15.131  
  15.132 -val prems = goal thy "(A == B) ==> |- A <-> B";
  15.133 +val prems = goal (the_context ()) "(A == B) ==> |- A <-> B";
  15.134  by (rewrite_goals_tac prems);
  15.135  by (rtac iff_refl 1);
  15.136  qed "def_imp_iff";
  15.137  
  15.138 -val prems = goal thy "(A == B) ==> |- A = B";
  15.139 +val prems = goal (the_context ()) "(A == B) ==> |- A = B";
  15.140  by (rewrite_goals_tac prems);
  15.141  by (rtac refl 1);
  15.142  qed "meta_eq_to_obj_eq";
    16.1 --- a/src/Sequents/LK0.thy	Sun Sep 18 14:25:48 2005 +0200
    16.2 +++ b/src/Sequents/LK0.thy	Sun Sep 18 15:20:08 2005 +0200
    16.3 @@ -1,136 +1,139 @@
    16.4 -(*  Title:      LK/LK0
    16.5 +(*  Title:      LK/LK0.thy
    16.6      ID:         $Id$
    16.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.8      Copyright   1993  University of Cambridge
    16.9  
   16.10 -Classical First-Order Sequent Calculus
   16.11 -
   16.12  There may be printing problems if a seqent is in expanded normal form
   16.13 -	(eta-expanded, beta-contracted)
   16.14 +        (eta-expanded, beta-contracted)
   16.15  *)
   16.16  
   16.17 -LK0 = Sequents +
   16.18 +header {* Classical First-Order Sequent Calculus *}
   16.19 +
   16.20 +theory LK0
   16.21 +imports Sequents
   16.22 +begin
   16.23  
   16.24  global
   16.25  
   16.26 -classes term
   16.27 -default term
   16.28 +classes "term"
   16.29 +defaultsort "term"
   16.30  
   16.31  consts
   16.32  
   16.33 - Trueprop	:: "two_seqi"
   16.34 + Trueprop       :: "two_seqi"
   16.35  
   16.36 -  True,False   :: o
   16.37 -  "="          :: ['a,'a] => o       (infixl 50)
   16.38 -  Not          :: o => o             ("~ _" [40] 40)
   16.39 -  "&"          :: [o,o] => o         (infixr 35)
   16.40 -  "|"          :: [o,o] => o         (infixr 30)
   16.41 -  "-->","<->"  :: [o,o] => o         (infixr 25)
   16.42 -  The          :: ('a => o) => 'a    (binder "THE " 10)
   16.43 -  All          :: ('a => o) => o     (binder "ALL " 10)
   16.44 -  Ex           :: ('a => o) => o     (binder "EX " 10)
   16.45 +  True         :: o
   16.46 +  False        :: o
   16.47 +  "="          :: "['a,'a] => o"     (infixl 50)
   16.48 +  Not          :: "o => o"           ("~ _" [40] 40)
   16.49 +  "&"          :: "[o,o] => o"       (infixr 35)
   16.50 +  "|"          :: "[o,o] => o"       (infixr 30)
   16.51 +  "-->"        :: "[o,o] => o"       (infixr 25)
   16.52 +  "<->"        :: "[o,o] => o"       (infixr 25)
   16.53 +  The          :: "('a => o) => 'a"  (binder "THE " 10)
   16.54 +  All          :: "('a => o) => o"   (binder "ALL " 10)
   16.55 +  Ex           :: "('a => o) => o"   (binder "EX " 10)
   16.56  
   16.57  syntax
   16.58 - "@Trueprop"	:: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
   16.59 -  "_not_equal" :: ['a, 'a] => o                (infixl "~=" 50)
   16.60 + "@Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
   16.61 +  "_not_equal" :: "['a, 'a] => o"              (infixl "~=" 50)
   16.62 +
   16.63 +parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
   16.64 +print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
   16.65  
   16.66  translations
   16.67    "x ~= y"      == "~ (x = y)"
   16.68  
   16.69  syntax (xsymbols)
   16.70 -  Not           :: o => o               ("\\<not> _" [40] 40)
   16.71 -  "op &"        :: [o, o] => o          (infixr "\\<and>" 35)
   16.72 -  "op |"        :: [o, o] => o          (infixr "\\<or>" 30)
   16.73 -  "op -->"      :: [o, o] => o          (infixr "\\<longrightarrow>" 25)
   16.74 -  "op <->"      :: [o, o] => o          (infixr "\\<longleftrightarrow>" 25)
   16.75 -  "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
   16.76 -  "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
   16.77 -  "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
   16.78 -  "_not_equal"  :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
   16.79 +  Not           :: "o => o"               ("\<not> _" [40] 40)
   16.80 +  "op &"        :: "[o, o] => o"          (infixr "\<and>" 35)
   16.81 +  "op |"        :: "[o, o] => o"          (infixr "\<or>" 30)
   16.82 +  "op -->"      :: "[o, o] => o"          (infixr "\<longrightarrow>" 25)
   16.83 +  "op <->"      :: "[o, o] => o"          (infixr "\<longleftrightarrow>" 25)
   16.84 +  "ALL "        :: "[idts, o] => o"       ("(3\<forall>_./ _)" [0, 10] 10)
   16.85 +  "EX "         :: "[idts, o] => o"       ("(3\<exists>_./ _)" [0, 10] 10)
   16.86 +  "EX! "        :: "[idts, o] => o"       ("(3\<exists>!_./ _)" [0, 10] 10)
   16.87 +  "_not_equal"  :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
   16.88  
   16.89  syntax (HTML output)
   16.90 -  Not           :: o => o               ("\\<not> _" [40] 40)
   16.91 -  "op &"        :: [o, o] => o          (infixr "\\<and>" 35)
   16.92 -  "op |"        :: [o, o] => o          (infixr "\\<or>" 30)
   16.93 -  "ALL "        :: [idts, o] => o       ("(3\\<forall>_./ _)" [0, 10] 10)
   16.94 -  "EX "         :: [idts, o] => o       ("(3\\<exists>_./ _)" [0, 10] 10)
   16.95 -  "EX! "        :: [idts, o] => o       ("(3\\<exists>!_./ _)" [0, 10] 10)
   16.96 -  "_not_equal"  :: ['a, 'a] => o        (infixl "\\<noteq>" 50)
   16.97 -
   16.98 +  Not           :: "o => o"               ("\<not> _" [40] 40)
   16.99 +  "op &"        :: "[o, o] => o"          (infixr "\<and>" 35)
  16.100 +  "op |"        :: "[o, o] => o"          (infixr "\<or>" 30)
  16.101 +  "ALL "        :: "[idts, o] => o"       ("(3\<forall>_./ _)" [0, 10] 10)
  16.102 +  "EX "         :: "[idts, o] => o"       ("(3\<exists>_./ _)" [0, 10] 10)
  16.103 +  "EX! "        :: "[idts, o] => o"       ("(3\<exists>!_./ _)" [0, 10] 10)
  16.104 +  "_not_equal"  :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
  16.105  
  16.106  local
  16.107 -  
  16.108 -rules
  16.109 +
  16.110 +axioms
  16.111  
  16.112    (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
  16.113  
  16.114 -  contRS "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F"
  16.115 -  contLS "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E"
  16.116 +  contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F"
  16.117 +  contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E"
  16.118  
  16.119 -  thinRS "$H |- $E, $F ==> $H |- $E, $S, $F"
  16.120 -  thinLS "$H, $G |- $E ==> $H, $S, $G |- $E"
  16.121 +  thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F"
  16.122 +  thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E"
  16.123  
  16.124 -  exchRS "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F"
  16.125 -  exchLS "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E"
  16.126 +  exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F"
  16.127 +  exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E"
  16.128  
  16.129 -  cut   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
  16.130 +  cut:   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
  16.131  
  16.132    (*Propositional rules*)
  16.133  
  16.134 -  basic "$H, P, $G |- $E, P, $F"
  16.135 +  basic: "$H, P, $G |- $E, P, $F"
  16.136  
  16.137 -  conjR "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
  16.138 -  conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
  16.139 +  conjR: "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
  16.140 +  conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
  16.141  
  16.142 -  disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
  16.143 -  disjL "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
  16.144 +  disjR: "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
  16.145 +  disjL: "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
  16.146  
  16.147 -  impR  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
  16.148 -  impL  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
  16.149 +  impR:  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
  16.150 +  impL:  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
  16.151  
  16.152 -  notR  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
  16.153 -  notL  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
  16.154 +  notR:  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
  16.155 +  notL:  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
  16.156  
  16.157 -  FalseL "$H, False, $G |- $E"
  16.158 +  FalseL: "$H, False, $G |- $E"
  16.159  
  16.160 -  True_def "True == False-->False"
  16.161 -  iff_def  "P<->Q == (P-->Q) & (Q-->P)"
  16.162 +  True_def: "True == False-->False"
  16.163 +  iff_def:  "P<->Q == (P-->Q) & (Q-->P)"
  16.164  
  16.165    (*Quantifiers*)
  16.166  
  16.167 -  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
  16.168 -  allL  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
  16.169 +  allR:  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
  16.170 +  allL:  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
  16.171  
  16.172 -  exR   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
  16.173 -  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
  16.174 +  exR:   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
  16.175 +  exL:   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
  16.176  
  16.177    (*Equality*)
  16.178  
  16.179 -  refl  "$H |- $E, a=a, $F"
  16.180 -  subst "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
  16.181 +  refl:  "$H |- $E, a=a, $F"
  16.182 +  subst: "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
  16.183  
  16.184    (* Reflection *)
  16.185  
  16.186 -  eq_reflection  "|- x=y ==> (x==y)"
  16.187 -  iff_reflection "|- P<->Q ==> (P==Q)"
  16.188 +  eq_reflection:  "|- x=y ==> (x==y)"
  16.189 +  iff_reflection: "|- P<->Q ==> (P==Q)"
  16.190  
  16.191    (*Descriptions*)
  16.192  
  16.193 -  The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> 
  16.194 +  The: "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==>
  16.195            $H |- $E, P(THE x. P(x)), $F"
  16.196  
  16.197  constdefs
  16.198 -  If :: [o, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
  16.199 +  If :: "[o, 'a, 'a] => 'a"   ("(if (_)/ then (_)/ else (_))" 10)
  16.200     "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
  16.201  
  16.202  setup
  16.203    prover_setup
  16.204  
  16.205 +ML {* use_legacy_bindings (the_context ()) *}
  16.206 +
  16.207  end
  16.208  
  16.209 -ML
  16.210  
  16.211 -
  16.212 -val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
  16.213 -val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
  16.214 -
    17.1 --- a/src/Sequents/Modal/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
    17.2 +++ b/src/Sequents/Modal/ROOT.ML	Sun Sep 18 15:20:08 2005 +0200
    17.3 @@ -1,21 +1,21 @@
    17.4 -(*  Title:      Modal/ex/ROOT
    17.5 +(*  Title:      Modal/ex/ROOT.ML
    17.6      ID:         $Id$
    17.7      Author:     Martin Coen
    17.8      Copyright   1991  University of Cambridge
    17.9  *)
   17.10  
   17.11  writeln "\nTheorems of T\n";
   17.12 -fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
   17.13 +fun try s = (writeln s; prove_goal (theory "T") s (fn _=> [T_Prover.solve_tac 2]));
   17.14  time_use "Tthms.ML";
   17.15  
   17.16  writeln "\nTheorems of S4\n";
   17.17 -fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2]));
   17.18 +fun try s = (writeln s; prove_goal (theory "S4") s (fn _=> [S4_Prover.solve_tac 2]));
   17.19  time_use "Tthms.ML";
   17.20  time_use "S4thms.ML";
   17.21  
   17.22  writeln "\nTheorems of S43\n";
   17.23  fun try s = (writeln s;
   17.24 -             prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE 
   17.25 +             prove_goal (theory "S43") s (fn _=> [S43_Prover.solve_tac 2 ORELSE
   17.26                                             S43_Prover.solve_tac 3]));
   17.27  time_use "Tthms.ML";
   17.28  time_use "S4thms.ML";
    18.1 --- a/src/Sequents/Modal0.ML	Sun Sep 18 14:25:48 2005 +0200
    18.2 +++ b/src/Sequents/Modal0.ML	Sun Sep 18 15:20:08 2005 +0200
    18.3 @@ -4,19 +4,19 @@
    18.4      Copyright   1991  University of Cambridge
    18.5  *)
    18.6  
    18.7 -structure Modal0_rls = 
    18.8 +structure Modal0_rls =
    18.9  struct
   18.10  
   18.11 -val rewrite_rls = [Modal0.strimp_def,Modal0.streqv_def];
   18.12 +val rewrite_rls = [strimp_def,streqv_def];
   18.13  
   18.14  local
   18.15 -  val iffR = prove_goal thy 
   18.16 +  val iffR = prove_goal (the_context ())
   18.17        "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
   18.18     (fn prems=>
   18.19      [ (rewtac iff_def),
   18.20        (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
   18.21  
   18.22 -  val iffL = prove_goal thy 
   18.23 +  val iffL = prove_goal (the_context ())
   18.24       "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
   18.25     (fn prems=>
   18.26      [ rewtac iff_def,
    19.1 --- a/src/Sequents/Modal0.thy	Sun Sep 18 14:25:48 2005 +0200
    19.2 +++ b/src/Sequents/Modal0.thy	Sun Sep 18 15:20:08 2005 +0200
    19.3 @@ -1,42 +1,43 @@
    19.4 -(*  Title:      Sequents/Modal0
    19.5 +(*  Title:      Sequents/Modal0.thy
    19.6      ID:         $Id$
    19.7      Author:     Martin Coen
    19.8      Copyright   1991  University of Cambridge
    19.9  *)
   19.10  
   19.11 -Modal0 = LK0 +
   19.12 +theory Modal0
   19.13 +imports LK0
   19.14 +uses "modal.ML"
   19.15 +begin
   19.16  
   19.17  consts
   19.18    box           :: "o=>o"       ("[]_" [50] 50)
   19.19    dia           :: "o=>o"       ("<>_" [50] 50)
   19.20 -  "--<",">-<"   :: "[o,o]=>o"   (infixr 25)
   19.21 -  Lstar,Rstar   :: "two_seqi"
   19.22 +  "--<"         :: "[o,o]=>o"   (infixr 25)
   19.23 +  ">-<"         :: "[o,o]=>o"   (infixr 25)
   19.24 +  Lstar         :: "two_seqi"
   19.25 +  Rstar         :: "two_seqi"
   19.26  
   19.27  syntax
   19.28    "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
   19.29    "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
   19.30  
   19.31 -rules
   19.32 -  (* Definitions *)
   19.33 -
   19.34 -  strimp_def    "P --< Q == [](P --> Q)"
   19.35 -  streqv_def    "P >-< Q == (P --< Q) & (Q --< P)"
   19.36 -end
   19.37 -
   19.38 -ML
   19.39 -
   19.40 -local
   19.41 -
   19.42 +ML {*
   19.43    val Lstar = "Lstar";
   19.44    val Rstar = "Rstar";
   19.45    val SLstar = "@Lstar";
   19.46    val SRstar = "@Rstar";
   19.47  
   19.48 -  fun star_tr c [s1,s2] =
   19.49 -      Const(c,dummyT)$Sequents.seq_tr s1$Sequents.seq_tr s2;
   19.50 -  fun star_tr' c [s1,s2] = 
   19.51 -      Const(c,dummyT) $ Sequents.seq_tr' s1 $ Sequents.seq_tr' s2;
   19.52 -in
   19.53 -val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
   19.54 -val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
   19.55 -end;
   19.56 +  fun star_tr c [s1,s2] = Const(c,dummyT)$ seq_tr s1$ seq_tr s2;
   19.57 +  fun star_tr' c [s1,s2] = Const(c,dummyT) $ seq_tr' s1 $ seq_tr' s2;
   19.58 +*}
   19.59 +
   19.60 +parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
   19.61 +print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
   19.62 +
   19.63 +defs
   19.64 +  strimp_def:    "P --< Q == [](P --> Q)"
   19.65 +  streqv_def:    "P >-< Q == (P --< Q) & (Q --< P)"
   19.66 +
   19.67 +ML {* use_legacy_bindings (the_context ()) *}
   19.68 +
   19.69 +end
    20.1 --- a/src/Sequents/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
    20.2 +++ b/src/Sequents/ROOT.ML	Sun Sep 18 15:20:08 2005 +0200
    20.3 @@ -3,29 +3,18 @@
    20.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    20.5      Copyright   1991  University of Cambridge
    20.6  
    20.7 -Adds Classical Sequent Calculus to a database containing pure Isabelle. 
    20.8 +Classical Sequent Calculus based on Pure Isabelle. 
    20.9  *)
   20.10  
   20.11  val banner = "Sequent Calculii";
   20.12  writeln banner;
   20.13  
   20.14 -print_depth 1;  
   20.15 -
   20.16  Unify.trace_bound:= 20;
   20.17  Unify.search_bound := 40;
   20.18  
   20.19 -use_thy "Sequents";
   20.20 -use "prover.ML";
   20.21 -
   20.22  use_thy "LK";
   20.23 -use "simpdata.ML";
   20.24 -
   20.25  use_thy "ILL";
   20.26 -
   20.27 -use "modal.ML";
   20.28  use_thy "Modal0";
   20.29  use_thy"T";
   20.30  use_thy"S4";
   20.31  use_thy"S43";
   20.32 -
   20.33 -print_depth 8;
    21.1 --- a/src/Sequents/S4.ML	Sun Sep 18 14:25:48 2005 +0200
    21.2 +++ b/src/Sequents/S4.ML	Sun Sep 18 15:20:08 2005 +0200
    21.3 @@ -1,10 +1,10 @@
    21.4 -(*  Title:      Modal/S4
    21.5 +(*  Title:      Modal/S4.ML
    21.6      ID:         $Id$
    21.7      Author:     Martin Coen
    21.8      Copyright   1991  University of Cambridge
    21.9  *)
   21.10  
   21.11 -local open Modal0_rls S4
   21.12 +local open Modal0_rls
   21.13  in structure MP_Rule : MODAL_PROVER_RULE =
   21.14     struct
   21.15      val rewrite_rls = rewrite_rls
    22.1 --- a/src/Sequents/S4.thy	Sun Sep 18 14:25:48 2005 +0200
    22.2 +++ b/src/Sequents/S4.thy	Sun Sep 18 15:20:08 2005 +0200
    22.3 @@ -1,31 +1,37 @@
    22.4 -(*  Title:      Modal/S4
    22.5 +(*  Title:      Modal/S4.thy
    22.6      ID:         $Id$
    22.7      Author:     Martin Coen
    22.8      Copyright   1991  University of Cambridge
    22.9  *)
   22.10  
   22.11 -S4 = Modal0 +
   22.12 -rules
   22.13 +theory S4
   22.14 +imports Modal0
   22.15 +begin
   22.16 +
   22.17 +axioms
   22.18  (* Definition of the star operation using a set of Horn clauses *)
   22.19  (* For system S4:  gamma * == {[]P | []P : gamma}               *)
   22.20  (*                 delta * == {<>P | <>P : delta}               *)
   22.21  
   22.22 -  lstar0         "|L>"
   22.23 -  lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
   22.24 -  lstar2         "$G |L> $H ==>   P, $G |L>      $H"
   22.25 -  rstar0         "|R>"
   22.26 -  rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
   22.27 -  rstar2         "$G |R> $H ==>   P, $G |R>      $H"
   22.28 +  lstar0:         "|L>"
   22.29 +  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
   22.30 +  lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
   22.31 +  rstar0:         "|R>"
   22.32 +  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
   22.33 +  rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
   22.34  
   22.35  (* Rules for [] and <> *)
   22.36  
   22.37 -  boxR
   22.38 -   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  
   22.39 +  boxR:
   22.40 +   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
   22.41             $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
   22.42 -  boxL     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
   22.43 +  boxL:     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
   22.44  
   22.45 -  diaR     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
   22.46 -  diaL
   22.47 -   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
   22.48 +  diaR:     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
   22.49 +  diaL:
   22.50 +   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
   22.51             $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
   22.52 +
   22.53 +ML {* use_legacy_bindings (the_context ()) *}
   22.54 +
   22.55  end
    23.1 --- a/src/Sequents/S43.ML	Sun Sep 18 14:25:48 2005 +0200
    23.2 +++ b/src/Sequents/S43.ML	Sun Sep 18 15:20:08 2005 +0200
    23.3 @@ -2,11 +2,9 @@
    23.4      ID:         $Id$
    23.5      Author:     Martin Coen
    23.6      Copyright   1991  University of Cambridge
    23.7 -
    23.8 -This implements Rajeev Gore's sequent calculus for S43.
    23.9  *)
   23.10  
   23.11 -local open Modal0_rls S43
   23.12 +local open Modal0_rls
   23.13  in structure MP_Rule : MODAL_PROVER_RULE =
   23.14     struct
   23.15      val rewrite_rls = rewrite_rls
   23.16 @@ -16,4 +14,4 @@
   23.17      val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2]
   23.18     end;
   23.19  end;
   23.20 -structure S43_Prover = Modal_ProverFun(MP_Rule);  
   23.21 +structure S43_Prover = Modal_ProverFun(MP_Rule);
    24.1 --- a/src/Sequents/S43.thy	Sun Sep 18 14:25:48 2005 +0200
    24.2 +++ b/src/Sequents/S43.thy	Sun Sep 18 15:20:08 2005 +0200
    24.3 @@ -1,4 +1,4 @@
    24.4 -(*  Title:      Modal/S43
    24.5 +(*  Title:      Modal/S43.thy
    24.6      ID:         $Id$
    24.7      Author:     Martin Coen
    24.8      Copyright   1991  University of Cambridge
    24.9 @@ -6,7 +6,9 @@
   24.10  This implements Rajeev Gore's sequent calculus for S43.
   24.11  *)
   24.12  
   24.13 -S43 = Modal0 +
   24.14 +theory S43
   24.15 +imports Modal0
   24.16 +begin
   24.17  
   24.18  consts
   24.19    S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
   24.20 @@ -15,17 +17,34 @@
   24.21    "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
   24.22                           ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
   24.23  
   24.24 -rules
   24.25 +ML {*
   24.26 +  val S43pi  = "S43pi";
   24.27 +  val SS43pi = "@S43pi";
   24.28 +
   24.29 +  val tr  = seq_tr;
   24.30 +  val tr' = seq_tr';
   24.31 +
   24.32 +  fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
   24.33 +        Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
   24.34 +  fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
   24.35 +        Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
   24.36 +
   24.37 +*}
   24.38 +
   24.39 +parse_translation {* [(SS43pi,s43pi_tr)] *}
   24.40 +print_translation {* [(S43pi,s43pi_tr')] *}
   24.41 +
   24.42 +axioms
   24.43  (* Definition of the star operation using a set of Horn clauses  *)
   24.44  (* For system S43: gamma * == {[]P | []P : gamma}                *)
   24.45  (*                 delta * == {<>P | <>P : delta}                *)
   24.46  
   24.47 -  lstar0         "|L>"
   24.48 -  lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
   24.49 -  lstar2         "$G |L> $H ==>   P, $G |L>      $H"
   24.50 -  rstar0         "|R>"
   24.51 -  rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
   24.52 -  rstar2         "$G |R> $H ==>   P, $G |R>      $H"
   24.53 +  lstar0:         "|L>"
   24.54 +  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
   24.55 +  lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
   24.56 +  rstar0:         "|R>"
   24.57 +  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
   24.58 +  rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
   24.59  
   24.60  (* Set of Horn clauses to generate the antecedents for the S43 pi rule       *)
   24.61  (* ie                                                                        *)
   24.62 @@ -37,43 +56,27 @@
   24.63  (*    and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj    *)
   24.64  (*    and 1<=i<=k and k<j<=k+m                                               *)
   24.65  
   24.66 -  S43pi0         "S43pi $L;; $R;; $Lbox; $Rdia"
   24.67 -  S43pi1
   24.68 -   "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==> 
   24.69 +  S43pi0:         "S43pi $L;; $R;; $Lbox; $Rdia"
   24.70 +  S43pi1:
   24.71 +   "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==>
   24.72         S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia"
   24.73 -  S43pi2
   24.74 -   "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==> 
   24.75 +  S43pi2:
   24.76 +   "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==>
   24.77         S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia"
   24.78  
   24.79  (* Rules for [] and <> for S43 *)
   24.80  
   24.81 -  boxL           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
   24.82 -  diaR           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
   24.83 -  pi1
   24.84 -   "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;  
   24.85 -      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 
   24.86 +  boxL:           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
   24.87 +  diaR:           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
   24.88 +  pi1:
   24.89 +   "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;
   24.90 +      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
   24.91     $L1, <>P, $L2 |- $R"
   24.92 -  pi2
   24.93 -   "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;  
   24.94 -      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 
   24.95 +  pi2:
   24.96 +   "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;
   24.97 +      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
   24.98     $L |- $R1, []P, $R2"
   24.99 -end
  24.100 -
  24.101 -ML
  24.102  
  24.103 -local
  24.104 -
  24.105 -  val S43pi  = "S43pi";
  24.106 -  val SS43pi = "@S43pi";
  24.107 -
  24.108 -  val tr  = Sequents.seq_tr;
  24.109 -  val tr' = Sequents.seq_tr';
  24.110 +ML {* use_legacy_bindings (the_context ()) *}
  24.111  
  24.112 -  fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
  24.113 -        Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
  24.114 -  fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
  24.115 -        Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
  24.116 -in
  24.117 -val parse_translation = [(SS43pi,s43pi_tr)];
  24.118 -val print_translation = [(S43pi,s43pi_tr')]
  24.119  end
    25.1 --- a/src/Sequents/Sequents.thy	Sun Sep 18 14:25:48 2005 +0200
    25.2 +++ b/src/Sequents/Sequents.thy	Sun Sep 18 15:20:08 2005 +0200
    25.3 @@ -1,29 +1,29 @@
    25.4 -(*  Title: 	Sequents/Sequents.thy
    25.5 +(*  Title:      Sequents/Sequents.thy
    25.6      ID:         $Id$
    25.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    25.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    25.9      Copyright   1993  University of Cambridge
   25.10 -
   25.11 -Basis theory for parsing and pretty-printing of sequences to be used in
   25.12 -Sequent Calculi. 
   25.13  *)
   25.14  
   25.15 -Sequents = Pure +
   25.16 +header {* Parsing and pretty-printing of sequences *}
   25.17 +
   25.18 +theory Sequents
   25.19 +imports Pure
   25.20 +uses ("prover.ML")
   25.21 +begin
   25.22  
   25.23  global
   25.24  
   25.25 -types
   25.26 -  o 
   25.27 -
   25.28 +typedecl o
   25.29  
   25.30  (* Sequences *)
   25.31  
   25.32 -types
   25.33 +typedecl
   25.34   seq'
   25.35  
   25.36  consts
   25.37 - SeqO'         :: [o,seq']=>seq'
   25.38 - Seq1'         :: o=>seq'
   25.39 -    
   25.40 + SeqO'         :: "[o,seq']=>seq'"
   25.41 + Seq1'         :: "o=>seq'"
   25.42 +
   25.43  
   25.44  (* concrete syntax *)
   25.45  
   25.46 @@ -32,37 +32,33 @@
   25.47  
   25.48  
   25.49  syntax
   25.50 - SeqEmp         :: seq                                ("")
   25.51 - SeqApp         :: [seqobj,seqcont] => seq            ("__")
   25.52 + SeqEmp         :: seq                                  ("")
   25.53 + SeqApp         :: "[seqobj,seqcont] => seq"            ("__")
   25.54  
   25.55 - SeqContEmp     :: seqcont                            ("")
   25.56 - SeqContApp     :: [seqobj,seqcont] => seqcont        (",/ __")
   25.57 -  
   25.58 - SeqO           :: o => seqobj                        ("_")
   25.59 - SeqId          :: 'a => seqobj                       ("$_")
   25.60 + SeqContEmp     :: seqcont                              ("")
   25.61 + SeqContApp     :: "[seqobj,seqcont] => seqcont"        (",/ __")
   25.62 +
   25.63 + SeqO           :: "o => seqobj"                        ("_")
   25.64 + SeqId          :: "'a => seqobj"                       ("$_")
   25.65  
   25.66  types
   25.67 -    
   25.68 - single_seqe = [seq,seqobj] => prop
   25.69 - single_seqi = [seq'=>seq',seq'=>seq'] => prop
   25.70 - two_seqi    = [seq'=>seq', seq'=>seq'] => prop
   25.71 - two_seqe    = [seq, seq] => prop
   25.72 - three_seqi  = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop
   25.73 - three_seqe  = [seq, seq, seq] => prop
   25.74 - four_seqi   = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop
   25.75 - four_seqe   = [seq, seq, seq, seq] => prop
   25.76 + single_seqe = "[seq,seqobj] => prop"
   25.77 + single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
   25.78 + two_seqi    = "[seq'=>seq', seq'=>seq'] => prop"
   25.79 + two_seqe    = "[seq, seq] => prop"
   25.80 + three_seqi  = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
   25.81 + three_seqe  = "[seq, seq, seq] => prop"
   25.82 + four_seqi   = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
   25.83 + four_seqe   = "[seq, seq, seq, seq] => prop"
   25.84  
   25.85 -
   25.86 - sequence_name = seq'=>seq'
   25.87 + sequence_name = "seq'=>seq'"
   25.88  
   25.89  
   25.90  syntax
   25.91    (*Constant to allow definitions of SEQUENCES of formulas*)
   25.92 -  "@Side"        :: seq=>(seq'=>seq')     ("<<(_)>>")
   25.93 +  "@Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
   25.94  
   25.95 -end
   25.96 -
   25.97 -ML
   25.98 +ML {*
   25.99  
  25.100  (* parse translation for sequences *)
  25.101  
  25.102 @@ -70,49 +66,49 @@
  25.103  
  25.104  fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
  25.105      seqobj_tr(_ $ i) = i;
  25.106 -    
  25.107 +
  25.108  fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
  25.109 -    seqcont_tr(Const("SeqContApp",_) $ so $ sc) = 
  25.110 +    seqcont_tr(Const("SeqContApp",_) $ so $ sc) =
  25.111        (seqobj_tr so) $ (seqcont_tr sc);
  25.112  
  25.113  fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
  25.114 -    seq_tr(Const("SeqApp",_) $ so $ sc) = 
  25.115 +    seq_tr(Const("SeqApp",_) $ so $ sc) =
  25.116        abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
  25.117  
  25.118  
  25.119  fun singlobj_tr(Const("SeqO",_) $ f) =
  25.120      abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
  25.121 -    
  25.122 +
  25.123  
  25.124 -    
  25.125 +
  25.126  (* print translation for sequences *)
  25.127  
  25.128 -fun seqcont_tr' (Bound 0) = 
  25.129 +fun seqcont_tr' (Bound 0) =
  25.130        Const("SeqContEmp",dummyT) |
  25.131      seqcont_tr' (Const("SeqO'",_) $ f $ s) =
  25.132 -      Const("SeqContApp",dummyT) $ 
  25.133 -      (Const("SeqO",dummyT) $ f) $ 
  25.134 +      Const("SeqContApp",dummyT) $
  25.135 +      (Const("SeqO",dummyT) $ f) $
  25.136        (seqcont_tr' s) |
  25.137 -(*    seqcont_tr' ((a as Abs(_,_,_)) $ s)= 
  25.138 +(*    seqcont_tr' ((a as Abs(_,_,_)) $ s)=
  25.139        seqcont_tr'(betapply(a,s)) | *)
  25.140 -    seqcont_tr' (i $ s) = 
  25.141 -      Const("SeqContApp",dummyT) $ 
  25.142 -      (Const("SeqId",dummyT) $ i) $ 
  25.143 +    seqcont_tr' (i $ s) =
  25.144 +      Const("SeqContApp",dummyT) $
  25.145 +      (Const("SeqId",dummyT) $ i) $
  25.146        (seqcont_tr' s);
  25.147  
  25.148  fun seq_tr' s =
  25.149 -    let fun seq_itr' (Bound 0) = 
  25.150 +    let fun seq_itr' (Bound 0) =
  25.151                Const("SeqEmp",dummyT) |
  25.152              seq_itr' (Const("SeqO'",_) $ f $ s) =
  25.153 -              Const("SeqApp",dummyT) $ 
  25.154 +              Const("SeqApp",dummyT) $
  25.155                (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
  25.156  (*            seq_itr' ((a as Abs(_,_,_)) $ s) =
  25.157                seq_itr'(betapply(a,s)) |    *)
  25.158              seq_itr' (i $ s) =
  25.159 -              Const("SeqApp",dummyT) $ 
  25.160 -              (Const("SeqId",dummyT) $ i) $ 
  25.161 +              Const("SeqApp",dummyT) $
  25.162 +              (Const("SeqId",dummyT) $ i) $
  25.163                (seqcont_tr' s)
  25.164 -    in case s of 
  25.165 +    in case s of
  25.166           Abs(_,_,t) => seq_itr' t |
  25.167           _ => s $ (Bound 0)
  25.168      end;
  25.169 @@ -138,22 +134,28 @@
  25.170  
  25.171  
  25.172  fun single_tr' c [s1, s2] =
  25.173 -(Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 ); 
  25.174 +(Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 );
  25.175  
  25.176  
  25.177  fun two_seq_tr' c [s1, s2] =
  25.178 -  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; 
  25.179 +  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
  25.180  
  25.181  fun three_seq_tr' c [s1, s2, s3] =
  25.182 -  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3; 
  25.183 +  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;
  25.184  
  25.185  fun four_seq_tr' c [s1, s2, s3, s4] =
  25.186 -  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4; 
  25.187 +  Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;
  25.188 +
  25.189  
  25.190  
  25.191 -			 
  25.192  (** for the <<...>> notation **)
  25.193 -  
  25.194 +
  25.195  fun side_tr [s1] = seq_tr s1;
  25.196 +*}
  25.197  
  25.198 -val parse_translation = [("@Side", side_tr)];
  25.199 +parse_translation {* [("@Side", side_tr)] *}
  25.200 +
  25.201 +use "prover.ML"
  25.202 +
  25.203 +end
  25.204 +
    26.1 --- a/src/Sequents/T.ML	Sun Sep 18 14:25:48 2005 +0200
    26.2 +++ b/src/Sequents/T.ML	Sun Sep 18 15:20:08 2005 +0200
    26.3 @@ -1,10 +1,10 @@
    26.4 -(*  Title:      Modal/T
    26.5 +(*  Title:      Modal/T.ML
    26.6      ID:         $Id$
    26.7      Author:     Martin Coen
    26.8      Copyright   1991  University of Cambridge
    26.9  *)
   26.10  
   26.11 -local open Modal0_rls T
   26.12 +local open Modal0_rls
   26.13  in structure MP_Rule : MODAL_PROVER_RULE =
   26.14     struct
   26.15      val rewrite_rls = rewrite_rls
   26.16 @@ -14,4 +14,4 @@
   26.17      val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2]
   26.18     end
   26.19  end;
   26.20 -structure T_Prover = Modal_ProverFun(MP_Rule);  
   26.21 +structure T_Prover = Modal_ProverFun(MP_Rule);
    27.1 --- a/src/Sequents/T.thy	Sun Sep 18 14:25:48 2005 +0200
    27.2 +++ b/src/Sequents/T.thy	Sun Sep 18 15:20:08 2005 +0200
    27.3 @@ -1,30 +1,36 @@
    27.4 -(*  Title:      Modal/T
    27.5 +(*  Title:      Modal/T.thy
    27.6      ID:         $Id$
    27.7      Author:     Martin Coen
    27.8      Copyright   1991  University of Cambridge
    27.9  *)
   27.10  
   27.11 -T = Modal0 +
   27.12 -rules
   27.13 +theory T
   27.14 +imports Modal0
   27.15 +begin
   27.16 +
   27.17 +axioms
   27.18  (* Definition of the star operation using a set of Horn clauses *)
   27.19  (* For system T:  gamma * == {P | []P : gamma}                  *)
   27.20  (*                delta * == {P | <>P : delta}                  *)
   27.21  
   27.22 -  lstar0         "|L>"
   27.23 -  lstar1         "$G |L> $H ==> []P, $G |L> P, $H"
   27.24 -  lstar2         "$G |L> $H ==>   P, $G |L>    $H"
   27.25 -  rstar0         "|R>"
   27.26 -  rstar1         "$G |R> $H ==> <>P, $G |R> P, $H"
   27.27 -  rstar2         "$G |R> $H ==>   P, $G |R>    $H"
   27.28 +  lstar0:         "|L>"
   27.29 +  lstar1:         "$G |L> $H ==> []P, $G |L> P, $H"
   27.30 +  lstar2:         "$G |L> $H ==>   P, $G |L>    $H"
   27.31 +  rstar0:         "|R>"
   27.32 +  rstar1:         "$G |R> $H ==> <>P, $G |R> P, $H"
   27.33 +  rstar2:         "$G |R> $H ==>   P, $G |R>    $H"
   27.34  
   27.35  (* Rules for [] and <> *)
   27.36  
   27.37 -  boxR
   27.38 -   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  
   27.39 +  boxR:
   27.40 +   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
   27.41                 $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
   27.42 -  boxL     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G"
   27.43 -  diaR     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
   27.44 -  diaL
   27.45 -   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  
   27.46 +  boxL:     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G"
   27.47 +  diaR:     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
   27.48 +  diaL:
   27.49 +   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
   27.50                 $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
   27.51 +
   27.52 +ML {* use_legacy_bindings (the_context ()) *}
   27.53 +
   27.54  end
    28.1 --- a/src/Sequents/simpdata.ML	Sun Sep 18 14:25:48 2005 +0200
    28.2 +++ b/src/Sequents/simpdata.ML	Sun Sep 18 15:20:08 2005 +0200
    28.3 @@ -12,7 +12,7 @@
    28.4  
    28.5  fun prove_fun s =
    28.6   (writeln s;
    28.7 -  prove_goal LK.thy s
    28.8 +  prove_goal (the_context ()) s
    28.9     (fn prems => [ (cut_facts_tac prems 1),
   28.10                    (fast_tac (pack() add_safes [subst]) 1) ]));
   28.11  
   28.12 @@ -144,7 +144,7 @@
   28.13  
   28.14  (*** Named rewrite rules ***)
   28.15  
   28.16 -fun prove nm thm  = qed_goal nm LK.thy thm
   28.17 +fun prove nm thm  = qed_goal nm (the_context ()) thm
   28.18      (fn prems => [ (cut_facts_tac prems 1),
   28.19                     (fast_tac LK_pack 1) ]);
   28.20  
   28.21 @@ -264,7 +264,7 @@
   28.22  
   28.23  (* To create substition rules *)
   28.24  
   28.25 -qed_goal "eq_imp_subst" LK.thy "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
   28.26 +qed_goal "eq_imp_subst" (the_context ()) "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
   28.27    (fn prems =>
   28.28     [cut_facts_tac prems 1,
   28.29      asm_simp_tac LK_basic_ss 1]);