--- 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"
--- 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]
--- 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 **)
--- 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"
--- 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 |] ==>
--- 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"
--- 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"