summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 28 Feb 2013 14:22:14 +0100 | |

changeset 51309 | 473303ef6e34 |

parent 51308 | 51e158e988a5 |

child 51310 | d2aeb3dffb8f |

eliminated legacy 'axioms';

--- 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"