# HG changeset patch
# User wenzelm
# Date 1362057734 -3600
# Node ID 473303ef6e34530b202660a3e7ec903dcb263e4e
# Parent  51e158e988a531d2150cc04bf86c375a451c8cd0
eliminated legacy 'axioms';

diff -r 51e158e988a5 -r 473303ef6e34 src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Thu Feb 28 14:10:54 2013 +0100
+++ b/src/Sequents/ILL.thy	Thu Feb 28 14:22:14 2013 +0100
@@ -54,47 +54,47 @@
 aneg_def:        "~A == A -o 0"
 
 
-axioms
+axiomatization where
 
-identity:        "P |- P"
+identity:        "P |- P" and
 
-zerol:           "$G, 0, $H |- A"
+zerol:           "$G, 0, $H |- A" and
 
   (* RULES THAT DO NOT DIVIDE CONTEXT *)
 
-derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C"
+derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C" and
   (* unfortunately, this one removes !A  *)
 
-contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
+contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C" and
 
-weaken:     "$F, $G |- C ==> $G, !A, $F |- C"
+weaken:     "$F, $G |- C ==> $G, !A, $F |- C" and
   (* weak form of weakening, in practice just to clean context *)
   (* weaken and contract not needed (CHECK)  *)
 
-promote2:        "promaux{ || $H || B} ==> $H |- !B"
+promote2:        "promaux{ || $H || B} ==> $H |- !B" and
 promote1:        "promaux{!A, $G || $H || B}
-                  ==> promaux {$G || $H, !A || B}"
-promote0:        "$G |- A ==> promaux {$G || || A}"
+                  ==> promaux {$G || $H, !A || B}" and
+promote0:        "$G |- A ==> promaux {$G || || A}" and
 
 
 
-tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
+tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C" and
 
-impr:      "A, $F |- B ==> $F |- A -o B"
+impr:      "A, $F |- B ==> $F |- A -o B" and
 
 conjr:           "[| $F |- A ;
                  $F |- B |]
-                ==> $F |- (A && B)"
+                ==> $F |- (A && B)" and
 
-conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C"
+conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C" and
 
-conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C"
+conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C" and
 
-disjrl:          "$G |- A ==> $G |- A ++ B"
-disjrr:          "$G |- B ==> $G |- A ++ B"
+disjrl:          "$G |- A ==> $G |- A ++ B" and
+disjrr:          "$G |- B ==> $G |- A ++ B" and
 disjl:           "[| $G, A, $H |- C ;
                      $G, B, $H |- C |]
-                 ==> $G, A ++ B, $H |- C"
+                 ==> $G, A ++ B, $H |- C" and
 
 
       (* RULES THAT DIVIDE CONTEXT *)
@@ -102,26 +102,26 @@
 tensr:           "[| $F, $J :=: $G;
                      $F |- A ;
                      $J |- B     |]
-                     ==> $G |- A >< B"
+                     ==> $G |- A >< B" and
 
 impl:            "[| $G, $F :=: $J, $H ;
                      B, $F |- C ;
                         $G |- A |]
-                     ==> $J, A -o B, $H |- C"
+                     ==> $J, A -o B, $H |- C" and
 
 
 cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
           $H1, $H2, $H3, $H4 |- A ;
-          $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
+          $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B" and
 
 
   (* CONTEXT RULES *)
 
-context1:     "$G :=: $G"
-context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
-context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
-context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
-context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
+context1:     "$G :=: $G" and
+context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G" and
+context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J" and
+context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G" and
+context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G" and
 context5:     "$F, $G :=: $H ==> $G, $F :=: $H"
 
 
diff -r 51e158e988a5 -r 473303ef6e34 src/Sequents/LK/Nat.thy
--- a/src/Sequents/LK/Nat.thy	Thu Feb 28 14:10:54 2013 +0100
+++ b/src/Sequents/LK/Nat.thy	Thu Feb 28 14:22:14 2013 +0100
@@ -11,20 +11,22 @@
 
 typedecl nat
 arities nat :: "term"
-consts  Zero :: nat      ("0")
-        Suc :: "nat=>nat"
-        rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
-        add :: "[nat, nat] => nat"                (infixl "+" 60)
 
-axioms
+axiomatization
+  Zero :: nat      ("0") and
+  Suc :: "nat=>nat" and
+  rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
+where
   induct:  "[| $H |- $E, P(0), $F;
-              !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
+              !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F" and
 
-  Suc_inject:  "|- Suc(m)=Suc(n) --> m=n"
-  Suc_neq_0:   "|- Suc(m) ~= 0"
-  rec_0:       "|- rec(0,a,f) = a"
+  Suc_inject:  "|- Suc(m)=Suc(n) --> m=n" and
+  Suc_neq_0:   "|- Suc(m) ~= 0" and
+  rec_0:       "|- rec(0,a,f) = a" and
   rec_Suc:     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
-  add_def:     "m+n == rec(m, n, %x y. Suc(y))"
+
+definition add :: "[nat, nat] => nat"  (infixl "+" 60)
+  where "m + n == rec(m, n, %x y. Suc(y))"
 
 
 declare Suc_neq_0 [simp]
diff -r 51e158e988a5 -r 473303ef6e34 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Thu Feb 28 14:10:54 2013 +0100
+++ b/src/Sequents/LK0.thy	Thu Feb 28 14:22:14 2013 +0100
@@ -59,67 +59,69 @@
   Ex  (binder "\<exists>" 10) and
   not_equal  (infixl "\<noteq>" 50)
 
-axioms
+axiomatization where
 
   (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
 
-  contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F"
-  contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E"
+  contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F" and
+  contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E" and
 
-  thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F"
-  thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E"
+  thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F" and
+  thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E" and
 
-  exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F"
-  exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E"
+  exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F" and
+  exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E" and
 
-  cut:   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
+  cut:   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E" and
 
   (*Propositional rules*)
 
-  basic: "$H, P, $G |- $E, P, $F"
+  basic: "$H, P, $G |- $E, P, $F" and
 
-  conjR: "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
-  conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
+  conjR: "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" and
+  conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" and
 
-  disjR: "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
-  disjL: "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
+  disjR: "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" and
+  disjL: "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" and
 
-  impR:  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
-  impL:  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
+  impR:  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" and
+  impL:  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" and
 
-  notR:  "$H, P |- $E, $F ==> $H |- $E, ~P, $F"
-  notL:  "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
+  notR:  "$H, P |- $E, $F ==> $H |- $E, ~P, $F" and
+  notL:  "$H, $G |- $E, P ==> $H, ~P, $G |- $E" and
 
-  FalseL: "$H, False, $G |- $E"
+  FalseL: "$H, False, $G |- $E" and
 
-  True_def: "True == False-->False"
+  True_def: "True == False-->False" and
   iff_def:  "P<->Q == (P-->Q) & (Q-->P)"
 
+axiomatization where
   (*Quantifiers*)
 
-  allR:  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
-  allL:  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
+  allR:  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F" and
+  allL:  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E" and
 
-  exR:   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
-  exL:   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
+  exR:   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F" and
+  exL:   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E" and
 
   (*Equality*)
-
-  refl:  "$H |- $E, a=a, $F"
-  subst: "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
+  refl:  "$H |- $E, a=a, $F" and
+  subst: "\<And>G H E. $H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
 
   (* Reflection *)
 
-  eq_reflection:  "|- x=y ==> (x==y)"
+axiomatization where
+  eq_reflection:  "|- x=y ==> (x==y)" and
   iff_reflection: "|- P<->Q ==> (P==Q)"
 
   (*Descriptions*)
 
+axiomatization where
   The: "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==>
           $H |- $E, P(THE x. P(x)), $F"
 
-definition If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) where 
-   "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
+definition If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
+  where "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
 
 
 (** Structural Rules on formulas **)
diff -r 51e158e988a5 -r 473303ef6e34 src/Sequents/S4.thy
--- a/src/Sequents/S4.thy	Thu Feb 28 14:10:54 2013 +0100
+++ b/src/Sequents/S4.thy	Thu Feb 28 14:22:14 2013 +0100
@@ -7,26 +7,26 @@
 imports Modal0
 begin
 
-axioms
+axiomatization where
 (* Definition of the star operation using a set of Horn clauses *)
 (* For system S4:  gamma * == {[]P | []P : gamma}               *)
 (*                 delta * == {<>P | <>P : delta}               *)
 
-  lstar0:         "|L>"
-  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
-  lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
-  rstar0:         "|R>"
-  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
-  rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
+  lstar0:         "|L>" and
+  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H" and
+  lstar2:         "$G |L> $H ==>   P, $G |L>      $H" and
+  rstar0:         "|R>" and
+  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H" and
+  rstar2:         "$G |R> $H ==>   P, $G |R>      $H" and
 
 (* Rules for [] and <> *)
 
   boxR:
    "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
-           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
-  boxL:     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
+           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G" and
+  boxL:     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G" and
 
-  diaR:     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
+  diaR:     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G" and
   diaL:
    "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
            $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
diff -r 51e158e988a5 -r 473303ef6e34 src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Thu Feb 28 14:10:54 2013 +0100
+++ b/src/Sequents/S43.thy	Thu Feb 28 14:22:14 2013 +0100
@@ -32,17 +32,17 @@
 in [(@{const_syntax S43pi}, s43pi_tr')] end
 *}
 
-axioms
+axiomatization where
 (* Definition of the star operation using a set of Horn clauses  *)
 (* For system S43: gamma * == {[]P | []P : gamma}                *)
 (*                 delta * == {<>P | <>P : delta}                *)
 
-  lstar0:         "|L>"
-  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
-  lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
-  rstar0:         "|R>"
-  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
-  rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
+  lstar0:         "|L>" and
+  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H" and
+  lstar2:         "$G |L> $H ==>   P, $G |L>      $H" and
+  rstar0:         "|R>" and
+  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H" and
+  rstar2:         "$G |R> $H ==>   P, $G |R>      $H" and
 
 (* Set of Horn clauses to generate the antecedents for the S43 pi rule       *)
 (* ie                                                                        *)
@@ -54,22 +54,22 @@
 (*    and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj    *)
 (*    and 1<=i<=k and k<j<=k+m                                               *)
 
-  S43pi0:         "S43pi $L;; $R;; $Lbox; $Rdia"
+  S43pi0:         "S43pi $L;; $R;; $Lbox; $Rdia" and
   S43pi1:
    "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==>
-       S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia"
+       S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia" and
   S43pi2:
    "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==>
-       S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia"
+       S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia" and
 
 (* Rules for [] and <> for S43 *)
 
-  boxL:           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
-  diaR:           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
+  boxL:           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G" and
+  diaR:           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G" and
   pi1:
    "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;
       S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
-   $L1, <>P, $L2 |- $R"
+   $L1, <>P, $L2 |- $R" and
   pi2:
    "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;
       S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
diff -r 51e158e988a5 -r 473303ef6e34 src/Sequents/T.thy
--- a/src/Sequents/T.thy	Thu Feb 28 14:10:54 2013 +0100
+++ b/src/Sequents/T.thy	Thu Feb 28 14:22:14 2013 +0100
@@ -7,25 +7,25 @@
 imports Modal0
 begin
 
-axioms
+axiomatization where
 (* Definition of the star operation using a set of Horn clauses *)
 (* For system T:  gamma * == {P | []P : gamma}                  *)
 (*                delta * == {P | <>P : delta}                  *)
 
-  lstar0:         "|L>"
-  lstar1:         "$G |L> $H ==> []P, $G |L> P, $H"
-  lstar2:         "$G |L> $H ==>   P, $G |L>    $H"
-  rstar0:         "|R>"
-  rstar1:         "$G |R> $H ==> <>P, $G |R> P, $H"
-  rstar2:         "$G |R> $H ==>   P, $G |R>    $H"
+  lstar0:         "|L>" and
+  lstar1:         "$G |L> $H ==> []P, $G |L> P, $H" and
+  lstar2:         "$G |L> $H ==>   P, $G |L>    $H" and
+  rstar0:         "|R>" and
+  rstar1:         "$G |R> $H ==> <>P, $G |R> P, $H" and
+  rstar2:         "$G |R> $H ==>   P, $G |R>    $H" and
 
 (* Rules for [] and <> *)
 
   boxR:
    "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
-               $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
-  boxL:     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G"
-  diaR:     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
+               $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G" and
+  boxL:     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G" and
+  diaR:     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G" and
   diaL:
    "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
                $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
diff -r 51e158e988a5 -r 473303ef6e34 src/Sequents/Washing.thy
--- a/src/Sequents/Washing.thy	Thu Feb 28 14:10:54 2013 +0100
+++ b/src/Sequents/Washing.thy	Thu Feb 28 14:22:14 2013 +0100
@@ -6,26 +6,25 @@
 imports ILL
 begin
 
-consts
-  dollar :: o
-  quarter :: o
-  loaded :: o
-  dirty :: o
-  wet :: o
+axiomatization
+  dollar :: o and
+  quarter :: o and
+  loaded :: o and
+  dirty :: o and
+  wet :: o and
   clean :: o
-
-axioms
+where
   change:
-  "dollar |- (quarter >< quarter >< quarter >< quarter)"
+  "dollar |- (quarter >< quarter >< quarter >< quarter)" and
 
   load1:
-  "quarter , quarter , quarter , quarter , quarter |- loaded"
+  "quarter , quarter , quarter , quarter , quarter |- loaded" and
 
   load2:
-  "dollar , quarter |- loaded"
+  "dollar , quarter |- loaded" and
 
   wash:
-  "loaded , dirty |- wet"
+  "loaded , dirty |- wet" and
 
   dry:
   "wet, quarter , quarter , quarter |- clean"