--- a/src/Sequents/ILL.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL.ML Sun Sep 18 15:20:08 2005 +0200
@@ -2,19 +2,18 @@
ID: $Id$
Author: Sara Kalvala and Valeria de Paiva
Copyright 1992 University of Cambridge
-
*)
val lazy_cs = empty_pack
add_safes [tensl, conjr, disjl, promote0,
- context2,context3]
+ context2,context3]
add_unsafes [identity, zerol, conjll, conjlr, disjrl, disjrr,
- impr, tensr, impl, derelict, weaken,
- promote1, promote2,context1,context4a,context4b];
+ impr, tensr, impl, derelict, weaken,
+ promote1, promote2,context1,context4a,context4b];
fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n);
-fun auto x = prove_goal thy x (fn prems => [best_tac lazy_cs 1]);
+fun auto x = prove_goal (the_context ()) x (fn prems => [best_tac lazy_cs 1]);
Goal "$F, $G |- A ==> $F, !(A -o B), $G |- B";
by (rtac derelict 1);
@@ -52,7 +51,7 @@
by (assume_tac 1);
qed "impr_contr_der";
-val _ = goal thy "$F, (!B) -o 0, $G, !B, $H |- A";
+val _ = goal (the_context ()) "$F, (!B) -o 0, $G, !B, $H |- A";
by (rtac impl 1);
by (rtac identity 3);
by (rtac context3 1);
@@ -61,7 +60,7 @@
qed "contrad1";
-val _ = goal thy "$F, !B, $G, (!B) -o 0, $H |- A";
+val _ = goal (the_context ()) "$F, !B, $G, (!B) -o 0, $H |- A";
by (rtac impl 1);
by (rtac identity 3);
by (rtac context3 1);
@@ -69,7 +68,7 @@
by (rtac zerol 1);
qed "contrad2";
-val _ = goal thy "A -o B, A |- B";
+val _ = goal (the_context ()) "A -o B, A |- B";
by (rtac impl 1);
by (rtac identity 2);
by (rtac identity 2);
@@ -94,7 +93,7 @@
by (rtac context1 1);
qed "mp_rule2";
-val _ = goal thy "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))";
+val _ = goal (the_context ()) "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))";
by (best_tac lazy_cs 1);
qed "or_to_and";
@@ -109,7 +108,7 @@
-val _ = goal thy "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C";
+val _ = goal (the_context ()) "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C";
by (rtac impr 1);
by (rtac conj_lemma 1);
by (rtac disjl 1);
@@ -136,20 +135,20 @@
qed "a_not_a_rule";
fun thm_to_rule x y =
- prove_goal thy x
+ prove_goal (the_context ()) x
(fn [prem] => [(rtac cut 1), (rtac y 2), (rtac prem 2),
- (best_tac lazy_cs 1)]);
+ (best_tac lazy_cs 1)]);
val safe_cs = lazy_cs add_safes [conj_lemma, ll_mp,contrad1,
- contrad2, mp_rule1, mp_rule2, o_a_rule,
- a_not_a_rule]
- add_unsafes [aux_impl];
+ contrad2, mp_rule1, mp_rule2, o_a_rule,
+ a_not_a_rule]
+ add_unsafes [aux_impl];
val power_cs = safe_cs add_unsafes [impr_contr_der];
-fun auto1 x = prove_goal thy x (fn prems => [best_tac safe_cs 1]) ;
+fun auto1 x = prove_goal (the_context ()) x (fn prems => [best_tac safe_cs 1]) ;
-fun auto2 x = prove_goal thy x (fn prems => [best_tac power_cs 1]) ;
+fun auto2 x = prove_goal (the_context ()) x (fn prems => [best_tac power_cs 1]) ;
(* some examples from Troelstra and van Dalen
--- a/src/Sequents/ILL.thy Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL.thy Sun Sep 18 15:20:08 2005 +0200
@@ -1,11 +1,12 @@
-(* Title: ILL.thy
+(* Title: Sequents/ILL.thy
ID: $Id$
Author: Sara Kalvala and Valeria de Paiva
Copyright 1995 University of Cambridge
*)
-
-ILL = Sequents +
+theory ILL
+imports Sequents
+begin
consts
Trueprop :: "two_seqi"
@@ -35,98 +36,93 @@
"@Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5)
"@PromAux" :: "three_seqe" ("promaux {_||_||_}")
+parse_translation {*
+ [("@Trueprop", single_tr "Trueprop"),
+ ("@Context", two_seq_tr "Context"),
+ ("@PromAux", three_seq_tr "PromAux")] *}
+
+print_translation {*
+ [("Trueprop", single_tr' "@Trueprop"),
+ ("Context", two_seq_tr'"@Context"),
+ ("PromAux", three_seq_tr'"@PromAux")] *}
+
defs
-liff_def "P o-o Q == (P -o Q) >< (Q -o P)"
+liff_def: "P o-o Q == (P -o Q) >< (Q -o P)"
-aneg_def "~A == A -o 0"
+aneg_def: "~A == A -o 0"
-
-
-rules
+axioms
-identity "P |- P"
+identity: "P |- P"
-zerol "$G, 0, $H |- A"
+zerol: "$G, 0, $H |- A"
(* RULES THAT DO NOT DIVIDE CONTEXT *)
-derelict "$F, A, $G |- C ==> $F, !A, $G |- C"
+derelict: "$F, A, $G |- C ==> $F, !A, $G |- C"
(* 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"
-weaken "$F, $G |- C ==> $G, !A, $F |- C"
+weaken: "$F, $G |- C ==> $G, !A, $F |- C"
(* weak form of weakening, in practice just to clean context *)
(* weaken and contract not needed (CHECK) *)
-promote2 "promaux{ || $H || B} ==> $H |- !B"
-promote1 "promaux{!A, $G || $H || B}
- ==> promaux {$G || $H, !A || B}"
-promote0 "$G |- A ==> promaux {$G || || A}"
+promote2: "promaux{ || $H || B} ==> $H |- !B"
+promote1: "promaux{!A, $G || $H || B}
+ ==> promaux {$G || $H, !A || B}"
+promote0: "$G |- A ==> promaux {$G || || A}"
-tensl "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
+tensl: "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
-impr "A, $F |- B ==> $F |- A -o B"
+impr: "A, $F |- B ==> $F |- A -o B"
-conjr "[| $F |- A ;
+conjr: "[| $F |- A ;
$F |- B |]
==> $F |- (A && B)"
-conjll "$G, A, $H |- C ==> $G, A && B, $H |- C"
+conjll: "$G, A, $H |- C ==> $G, A && B, $H |- C"
-conjlr "$G, B, $H |- C ==> $G, A && B, $H |- C"
+conjlr: "$G, B, $H |- C ==> $G, A && B, $H |- C"
-disjrl "$G |- A ==> $G |- A ++ B"
-disjrr "$G |- B ==> $G |- A ++ B"
-disjl "[| $G, A, $H |- C ;
- $G, B, $H |- C |]
- ==> $G, A ++ B, $H |- C"
+disjrl: "$G |- A ==> $G |- A ++ B"
+disjrr: "$G |- B ==> $G |- A ++ B"
+disjl: "[| $G, A, $H |- C ;
+ $G, B, $H |- C |]
+ ==> $G, A ++ B, $H |- C"
(* RULES THAT DIVIDE CONTEXT *)
-tensr "[| $F, $J :=: $G;
- $F |- A ;
- $J |- B |]
- ==> $G |- A >< B"
+tensr: "[| $F, $J :=: $G;
+ $F |- A ;
+ $J |- B |]
+ ==> $G |- A >< B"
-impl "[| $G, $F :=: $J, $H ;
- B, $F |- C ;
- $G |- A |]
- ==> $J, A -o B, $H |- C"
+impl: "[| $G, $F :=: $J, $H ;
+ B, $F |- C ;
+ $G |- A |]
+ ==> $J, A -o B, $H |- C"
-cut " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
- $H1, $H2, $H3, $H4 |- A ;
- $J1, $J2, A, $J3, $J4 |- B |] ==> $F |- B"
+cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
+ $H1, $H2, $H3, $H4 |- A ;
+ $J1, $J2, A, $J3, $J4 |- B |] ==> $F |- B"
(* 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"
-context5 "$F, $G :=: $H ==> $G, $F :=: $H"
+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"
+context5: "$F, $G :=: $H ==> $G, $F :=: $H"
-
-
+ML {* use_legacy_bindings (the_context ()) *}
end
-
-ML
-
-val parse_translation = [("@Trueprop",Sequents.single_tr "Trueprop"),
- ("@Context",Sequents.two_seq_tr "Context"),
- ("@PromAux", Sequents.three_seq_tr "PromAux")];
-
-val print_translation = [("Trueprop",Sequents.single_tr' "@Trueprop"),
- ("Context",Sequents.two_seq_tr'"@Context"),
- ("PromAux", Sequents.three_seq_tr'"@PromAux")];
-
-
--- a/src/Sequents/ILL/ILL_predlog.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL/ILL_predlog.ML Sun Sep 18 15:20:08 2005 +0200
@@ -1,6 +1,6 @@
-fun auto1 x = prove_goal thy x
+fun auto1 x = prove_goal (the_context ()) x
(fn prems => [best_tac safe_cs 1]) ;
-fun auto2 x = prove_goal thy x
+fun auto2 x = prove_goal (the_context ()) x
(fn prems => [best_tac power_cs 1]) ;
--- a/src/Sequents/ILL/ILL_predlog.thy Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL/ILL_predlog.thy Sun Sep 18 15:20:08 2005 +0200
@@ -1,36 +1,32 @@
-(*
- File: /Nfs/toton/usr20/sk/isa_files/ll/NEW/pred_log.thy
- Theory Name: pred_log
- Logic Image: HOL
-*)
+(* $Id$ *)
-ILL_predlog = ILL +
+theory ILL_predlog
+imports ILL
+begin
-types
- plf
-
+typedecl plf
+
consts
-
"&" :: "[plf,plf] => plf" (infixr 35)
"|" :: "[plf,plf] => plf" (infixr 35)
">" :: "[plf,plf] => plf" (infixr 35)
"=" :: "[plf,plf] => plf" (infixr 35)
"@NG" :: "plf => plf" ("- _ " [50] 55)
ff :: "plf"
-
+
PL :: "plf => o" ("[* / _ / *]" [] 100)
translations
- "[* A & B *]" == "[*A*] && [*B*]"
+ "[* A & B *]" == "[*A*] && [*B*]"
"[* A | B *]" == "![*A*] ++ ![*B*]"
"[* - A *]" == "[*A > ff*]"
"[* ff *]" == "0"
"[* A = B *]" => "[* (A > B) & (B > A) *]"
-
+
"[* A > B *]" == "![*A*] -o [*B*]"
-
+
(* another translations for linear implication:
"[* A > B *]" == "!([*A*] -o [*B*])" *)
--- a/src/Sequents/ILL/ROOT.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL/ROOT.ML Sun Sep 18 15:20:08 2005 +0200
@@ -1,3 +1,4 @@
+(* $Id$ *)
time_use_thy "washing";
time_use_thy "ILL_predlog";
--- a/src/Sequents/ILL/washing.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL/washing.ML Sun Sep 18 15:20:08 2005 +0200
@@ -1,3 +1,5 @@
+(* $Id$ *)
+
(* "activate" definitions for use in proof *)
val changeI = [context1] RL ([change] RLN (2,[cut]));
@@ -16,15 +18,11 @@
(* order of premises doesn't matter *)
-prove_goal thy "dollar , dirty , dollar |- clean"
+prove_goal (the_context ()) "dollar , dirty , dollar |- clean"
(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
(* alternative formulation *)
-prove_goal thy "dollar , dollar |- dirty -o clean"
+prove_goal (the_context ()) "dollar , dollar |- dirty -o clean"
(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
-
-
-
-
--- a/src/Sequents/ILL/washing.thy Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ILL/washing.thy Sun Sep 18 15:20:08 2005 +0200
@@ -1,33 +1,38 @@
-
-(* code by Sara Kalvala, based on Paulson's LK
+(* $Id$ *)
+
+(* code by Sara Kalvala, based on Paulson's LK
and Moore's tisl.ML *)
-washing = ILL +
+theory washing
+imports ILL
+begin
consts
-
-dollar,quarter,loaded,dirty,wet,clean :: "o"
+ dollar :: o
+ quarter :: o
+ loaded :: o
+ dirty :: o
+ wet :: o
+ clean :: o
-
-rules
-
-
- change
+axioms
+ change:
"dollar |- (quarter >< quarter >< quarter >< quarter)"
- load1
+ load1:
"quarter , quarter , quarter , quarter , quarter |- loaded"
- load2
+ load2:
"dollar , quarter |- loaded"
- wash
+ wash:
"loaded , dirty |- wet"
- dry
+ dry:
"wet, quarter , quarter , quarter |- clean"
+ML {* use_legacy_bindings (the_context ()) *}
+
end
-
\ No newline at end of file
--- a/src/Sequents/LK.thy Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK.thy Sun Sep 18 15:20:08 2005 +0200
@@ -1,4 +1,4 @@
-(* Title: LK/LK
+(* Title: LK/LK.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -13,12 +13,20 @@
various modal rules would become inconsistent.
*)
-LK = LK0 +
+theory LK
+imports LK0
+uses ("simpdata.ML")
+begin
-rules
+axioms
+
+ monotonic: "($H |- P ==> $H |- Q) ==> $H, P |- Q"
- monotonic "($H |- P ==> $H |- Q) ==> $H, P |- Q"
+ left_cong: "[| P == P'; |- P' ==> ($H |- $F) == ($H' |- $F') |]
+ ==> (P, $H |- $F) == (P', $H' |- $F')"
- left_cong "[| P == P'; |- P' ==> ($H |- $F) == ($H' |- $F') |]
- ==> (P, $H |- $F) == (P', $H' |- $F')"
+ML {* use_legacy_bindings (the_context ()) *}
+
+use "simpdata.ML"
+
end
--- a/src/Sequents/LK/Nat.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK/Nat.ML Sun Sep 18 15:20:08 2005 +0200
@@ -1,9 +1,7 @@
-(* Title: Sequents/LK/Nat
+(* Title: Sequents/LK/Nat.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1999 University of Cambridge
-
-Theory of the natural numbers: Peano's axioms, primitive recursion
*)
Addsimps [Suc_neq_0];
--- a/src/Sequents/LK/Nat.thy Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK/Nat.thy Sun Sep 18 15:20:08 2005 +0200
@@ -1,26 +1,32 @@
-(* Title: Sequents/LK/Nat
+(* Title: Sequents/LK/Nat.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1999 University of Cambridge
-
-Theory of the natural numbers: Peano's axioms, primitive recursion
*)
-Nat = LK +
-types nat
-arities nat :: term
+header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
+
+theory Nat
+imports LK
+begin
+
+typedecl nat
+arities nat :: "term"
consts "0" :: nat ("0")
- Suc :: nat=>nat
- rec :: [nat, 'a, [nat,'a]=>'a] => 'a
- "+" :: [nat, nat] => nat (infixl 60)
+ Suc :: "nat=>nat"
+ rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
+ "+" :: "[nat, nat] => nat" (infixl 60)
-rules
- induct "[| $H |- $E, P(0), $F;
+axioms
+ induct: "[| $H |- $E, P(0), $F;
!!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F"
- Suc_inject "|- Suc(m)=Suc(n) --> m=n"
- Suc_neq_0 "|- Suc(m) ~= 0"
- rec_0 "|- rec(0,a,f) = a"
- rec_Suc "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
- add_def "m+n == rec(m, n, %x y. Suc(y))"
+ Suc_inject: "|- Suc(m)=Suc(n) --> m=n"
+ Suc_neq_0: "|- Suc(m) ~= 0"
+ rec_0: "|- rec(0,a,f) = a"
+ rec_Suc: "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
+ add_def: "m+n == rec(m, n, %x y. Suc(y))"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/Sequents/LK/ROOT.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK/ROOT.ML Sun Sep 18 15:20:08 2005 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Executes all examples for Classical Logic.
+Examples for Classical Logic.
*)
time_use "prop.ML";
--- a/src/Sequents/LK/hardquant.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK/hardquant.ML Sun Sep 18 15:20:08 2005 +0200
@@ -12,25 +12,23 @@
Uses pc_tac rather than fast_tac when the former is significantly faster.
*)
-writeln"File LK/ex/hard-quant.";
-
-context LK.thy;
+context (theory "LK");
Goal "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
by (Fast_tac 1);
-result();
+result();
Goal "|- (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))";
by (Fast_tac 1);
-result();
+result();
Goal "|- (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q";
by (Fast_tac 1);
-result();
+result();
Goal "|- (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)";
by (Fast_tac 1);
-result();
+result();
writeln"Problems requiring quantifier duplication";
@@ -53,7 +51,7 @@
writeln"Problem 18";
Goal "|- EX y. ALL x. P(y)-->P(x)";
by (best_tac LK_dup_pack 1);
-result();
+result();
writeln"Problem 19";
Goal "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
@@ -63,7 +61,7 @@
writeln"Problem 20";
Goal "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) \
\ --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
-by (Fast_tac 1);
+by (Fast_tac 1);
result();
writeln"Problem 21";
@@ -73,12 +71,12 @@
writeln"Problem 22";
Goal "|- (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))";
-by (Fast_tac 1);
+by (Fast_tac 1);
result();
writeln"Problem 23";
Goal "|- (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))";
-by (best_tac LK_pack 1);
+by (best_tac LK_pack 1);
result();
writeln"Problem 24";
@@ -94,7 +92,7 @@
\ (ALL x. P(x) --> (M(x) & L(x))) & \
\ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) \
\ --> (EX x. Q(x)&P(x))";
-by (best_tac LK_pack 1);
+by (best_tac LK_pack 1);
result();
writeln"Problem 26";
@@ -110,7 +108,7 @@
\ (ALL x. M(x) & L(x) --> P(x)) & \
\ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) \
\ --> (ALL x. M(x) --> ~L(x))";
-by (pc_tac LK_pack 1);
+by (pc_tac LK_pack 1);
result();
writeln"Problem 28. AMENDED";
@@ -118,21 +116,21 @@
\ ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & \
\ ((EX x. S(x)) --> (ALL x. L(x) --> M(x))) \
\ --> (ALL x. P(x) & L(x) --> M(x))";
-by (pc_tac LK_pack 1);
+by (pc_tac LK_pack 1);
result();
writeln"Problem 29. Essentially the same as Principia Mathematica *11.71";
Goal "|- (EX x. P(x)) & (EX y. Q(y)) \
\ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> \
\ (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
-by (pc_tac LK_pack 1);
+by (pc_tac LK_pack 1);
result();
writeln"Problem 30";
Goal "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & \
\ (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \
\ --> (ALL x. S(x))";
-by (Fast_tac 1);
+by (Fast_tac 1);
result();
writeln"Problem 31";
@@ -238,7 +236,7 @@
\ (EX x. f(x) & (ALL y. h(x,y) --> l(y)) \
\ & (ALL y. g(y) & h(x,y) --> j(x,y))) \
\ --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
-by (best_tac LK_pack 1);
+by (best_tac LK_pack 1);
result();
@@ -249,7 +247,7 @@
by (fast_tac (pack() add_safes [subst]) 1);
result();
-writeln"Problem 50";
+writeln"Problem 50";
Goal "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
by (best_tac LK_dup_pack 1);
result();
@@ -287,7 +285,7 @@
writeln"Problem 59";
(*Unification works poorly here -- the abstraction %sobj prevents efficient
operation of the occurs check*)
-Unify.trace_bound := !Unify.search_bound - 1;
+Unify.trace_bound := !Unify.search_bound - 1;
Goal "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
by (best_tac LK_dup_pack 1);
result();
@@ -304,8 +302,7 @@
by (Fast_tac 1);
result();
-writeln"Reached end of file.";
-
(*18 June 92: loaded in 372 secs*)
(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
(*29 June 92: loaded in 370 secs*)
+(*18 September 2005: loaded in 1.809 secs*)
--- a/src/Sequents/LK/prop.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK/prop.ML Sun Sep 18 15:20:08 2005 +0200
@@ -7,93 +7,91 @@
Can be read to test the LK system.
*)
-writeln"LK/ex/prop: propositional examples";
-
writeln"absorptive laws of & and | ";
-goal LK.thy "|- P & P <-> P";
+goal (theory "LK") "|- P & P <-> P";
by (fast_tac prop_pack 1);
result();
-goal LK.thy "|- P | P <-> P";
+goal (theory "LK") "|- P | P <-> P";
by (fast_tac prop_pack 1);
result();
writeln"commutative laws of & and | ";
-goal LK.thy "|- P & Q <-> Q & P";
+goal (theory "LK") "|- P & Q <-> Q & P";
by (fast_tac prop_pack 1);
result();
-goal LK.thy "|- P | Q <-> Q | P";
+goal (theory "LK") "|- P | Q <-> Q | P";
by (fast_tac prop_pack 1);
result();
writeln"associative laws of & and | ";
-goal LK.thy "|- (P & Q) & R <-> P & (Q & R)";
+goal (theory "LK") "|- (P & Q) & R <-> P & (Q & R)";
by (fast_tac prop_pack 1);
result();
-goal LK.thy "|- (P | Q) | R <-> P | (Q | R)";
+goal (theory "LK") "|- (P | Q) | R <-> P | (Q | R)";
by (fast_tac prop_pack 1);
result();
writeln"distributive laws of & and | ";
-goal LK.thy "|- (P & Q) | R <-> (P | R) & (Q | R)";
+goal (theory "LK") "|- (P & Q) | R <-> (P | R) & (Q | R)";
by (fast_tac prop_pack 1);
result();
-goal LK.thy "|- (P | Q) & R <-> (P & R) | (Q & R)";
+goal (theory "LK") "|- (P | Q) & R <-> (P & R) | (Q & R)";
by (fast_tac prop_pack 1);
result();
writeln"Laws involving implication";
-goal LK.thy "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
+goal (theory "LK") "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
by (fast_tac prop_pack 1);
result();
-goal LK.thy "|- (P & Q --> R) <-> (P--> (Q-->R))";
+goal (theory "LK") "|- (P & Q --> R) <-> (P--> (Q-->R))";
by (fast_tac prop_pack 1);
result();
-goal LK.thy "|- (P --> Q & R) <-> (P-->Q) & (P-->R)";
+goal (theory "LK") "|- (P --> Q & R) <-> (P-->Q) & (P-->R)";
by (fast_tac prop_pack 1);
result();
writeln"Classical theorems";
-goal LK.thy "|- P|Q --> P| ~P&Q";
+goal (theory "LK") "|- P|Q --> P| ~P&Q";
by (fast_tac prop_pack 1);
result();
-goal LK.thy "|- (P-->Q)&(~P-->R) --> (P&Q | R)";
+goal (theory "LK") "|- (P-->Q)&(~P-->R) --> (P&Q | R)";
by (fast_tac prop_pack 1);
result();
-goal LK.thy "|- P&Q | ~P&R <-> (P-->Q)&(~P-->R)";
+goal (theory "LK") "|- P&Q | ~P&R <-> (P-->Q)&(~P-->R)";
by (fast_tac prop_pack 1);
result();
-goal LK.thy "|- (P-->Q) | (P-->R) <-> (P --> Q | R)";
+goal (theory "LK") "|- (P-->Q) | (P-->R) <-> (P --> Q | R)";
by (fast_tac prop_pack 1);
result();
(*If and only if*)
-goal LK.thy "|- (P<->Q) <-> (Q<->P)";
+goal (theory "LK") "|- (P<->Q) <-> (Q<->P)";
by (fast_tac prop_pack 1);
result();
-goal LK.thy "|- ~ (P <-> ~P)";
+goal (theory "LK") "|- ~ (P <-> ~P)";
by (fast_tac prop_pack 1);
result();
@@ -106,89 +104,87 @@
*)
(*1*)
-goal LK.thy "|- (P-->Q) <-> (~Q --> ~P)";
+goal (theory "LK") "|- (P-->Q) <-> (~Q --> ~P)";
by (fast_tac prop_pack 1);
result();
(*2*)
-goal LK.thy "|- ~ ~ P <-> P";
+goal (theory "LK") "|- ~ ~ P <-> P";
by (fast_tac prop_pack 1);
result();
(*3*)
-goal LK.thy "|- ~(P-->Q) --> (Q-->P)";
+goal (theory "LK") "|- ~(P-->Q) --> (Q-->P)";
by (fast_tac prop_pack 1);
result();
(*4*)
-goal LK.thy "|- (~P-->Q) <-> (~Q --> P)";
+goal (theory "LK") "|- (~P-->Q) <-> (~Q --> P)";
by (fast_tac prop_pack 1);
result();
(*5*)
-goal LK.thy "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
+goal (theory "LK") "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
by (fast_tac prop_pack 1);
result();
(*6*)
-goal LK.thy "|- P | ~ P";
+goal (theory "LK") "|- P | ~ P";
by (fast_tac prop_pack 1);
result();
(*7*)
-goal LK.thy "|- P | ~ ~ ~ P";
+goal (theory "LK") "|- P | ~ ~ ~ P";
by (fast_tac prop_pack 1);
result();
(*8. Peirce's law*)
-goal LK.thy "|- ((P-->Q) --> P) --> P";
+goal (theory "LK") "|- ((P-->Q) --> P) --> P";
by (fast_tac prop_pack 1);
result();
(*9*)
-goal LK.thy "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
+goal (theory "LK") "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
by (fast_tac prop_pack 1);
result();
(*10*)
-goal LK.thy "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
+goal (theory "LK") "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
by (fast_tac prop_pack 1);
result();
(*11. Proved in each direction (incorrectly, says Pelletier!!) *)
-goal LK.thy "|- P<->P";
+goal (theory "LK") "|- P<->P";
by (fast_tac prop_pack 1);
result();
(*12. "Dijkstra's law"*)
-goal LK.thy "|- ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))";
+goal (theory "LK") "|- ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))";
by (fast_tac prop_pack 1);
result();
(*13. Distributive law*)
-goal LK.thy "|- P | (Q & R) <-> (P | Q) & (P | R)";
+goal (theory "LK") "|- P | (Q & R) <-> (P | Q) & (P | R)";
by (fast_tac prop_pack 1);
result();
(*14*)
-goal LK.thy "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
+goal (theory "LK") "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
by (fast_tac prop_pack 1);
result();
(*15*)
-goal LK.thy "|- (P --> Q) <-> (~P | Q)";
+goal (theory "LK") "|- (P --> Q) <-> (~P | Q)";
by (fast_tac prop_pack 1);
result();
(*16*)
-goal LK.thy "|- (P-->Q) | (Q-->P)";
+goal (theory "LK") "|- (P-->Q) | (Q-->P)";
by (fast_tac prop_pack 1);
result();
(*17*)
-goal LK.thy "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
+goal (theory "LK") "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
by (fast_tac prop_pack 1);
result();
-
-writeln"Reached end of file.";
--- a/src/Sequents/LK/quant.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK/quant.ML Sun Sep 18 15:20:08 2005 +0200
@@ -1,4 +1,4 @@
-(* Title: LK/ex/quant
+(* Title: LK/ex/quant.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
@@ -6,155 +6,151 @@
Classical sequent calculus: examples with quantifiers.
*)
-
-writeln"LK/ex/quant: Examples with quantifiers";
-
-goal LK.thy "|- (ALL x. P) <-> P";
+goal (theory "LK") "|- (ALL x. P) <-> P";
by (fast_tac LK_pack 1);
-result();
+result();
-goal LK.thy "|- (ALL x y. P(x,y)) <-> (ALL y x. P(x,y))";
+goal (theory "LK") "|- (ALL x y. P(x,y)) <-> (ALL y x. P(x,y))";
by (fast_tac LK_pack 1);
-result();
+result();
-goal LK.thy "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)";
+goal (theory "LK") "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)";
by (fast_tac LK_pack 1);
-result();
+result();
writeln"Permutation of existential quantifier.";
-goal LK.thy "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))";
+goal (theory "LK") "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))";
by (fast_tac LK_pack 1);
-result();
+result();
-goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
+goal (theory "LK") "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
by (fast_tac LK_pack 1);
-result();
+result();
(*Converse is invalid*)
-goal LK.thy "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))";
+goal (theory "LK") "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))";
by (fast_tac LK_pack 1);
-result();
+result();
writeln"Pushing ALL into an implication.";
-goal LK.thy "|- (ALL x. P --> Q(x)) <-> (P --> (ALL x. Q(x)))";
+goal (theory "LK") "|- (ALL x. P --> Q(x)) <-> (P --> (ALL x. Q(x)))";
by (fast_tac LK_pack 1);
-result();
+result();
-goal LK.thy "|- (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)";
+goal (theory "LK") "|- (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)";
by (fast_tac LK_pack 1);
-result();
+result();
-goal LK.thy "|- (EX x. P) <-> P";
+goal (theory "LK") "|- (EX x. P) <-> P";
by (fast_tac LK_pack 1);
-result();
+result();
writeln"Distribution of EX over disjunction.";
-goal LK.thy "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
+goal (theory "LK") "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
by (fast_tac LK_pack 1);
-result();
+result();
(*5 secs*)
(*Converse is invalid*)
-goal LK.thy "|- (EX x. P(x) & Q(x)) --> (EX x. P(x)) & (EX x. Q(x))";
+goal (theory "LK") "|- (EX x. P(x) & Q(x)) --> (EX x. P(x)) & (EX x. Q(x))";
by (fast_tac LK_pack 1);
-result();
+result();
writeln"Harder examples: classical theorems.";
-goal LK.thy "|- (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))";
+goal (theory "LK") "|- (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))";
by (fast_tac LK_pack 1);
-result();
+result();
(*3 secs*)
-goal LK.thy "|- (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q";
+goal (theory "LK") "|- (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q";
by (fast_tac LK_pack 1);
-result();
+result();
(*5 secs*)
-goal LK.thy "|- (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)";
+goal (theory "LK") "|- (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)";
by (fast_tac LK_pack 1);
-result();
+result();
writeln"Basic test of quantifier reasoning";
-goal LK.thy
+goal (theory "LK")
"|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
by (fast_tac LK_pack 1);
-result();
+result();
-goal LK.thy "|- (ALL x. Q(x)) --> (EX x. Q(x))";
+goal (theory "LK") "|- (ALL x. Q(x)) --> (EX x. Q(x))";
by (fast_tac LK_pack 1);
-result();
+result();
writeln"The following are invalid!";
(*INVALID*)
-goal LK.thy "|- (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))";
-by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
+goal (theory "LK") "|- (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))";
+by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
-getgoal 1;
+getgoal 1;
(*INVALID*)
-goal LK.thy "|- (EX x. Q(x)) --> (ALL x. Q(x))";
+goal (theory "LK") "|- (EX x. Q(x)) --> (ALL x. Q(x))";
by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
-getgoal 1;
+getgoal 1;
-goal LK.thy "|- P(?a) --> (ALL x. P(x))";
+goal (theory "LK") "|- P(?a) --> (ALL x. P(x))";
by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
-getgoal 1;
+getgoal 1;
-goal LK.thy "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
+goal (theory "LK") "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
-getgoal 1;
+getgoal 1;
writeln"Back to things that are provable...";
-goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
-by (fast_tac LK_pack 1);
-result();
+goal (theory "LK") "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
+by (fast_tac LK_pack 1);
+result();
(*An example of why exR should be delayed as long as possible*)
-goal LK.thy "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))";
+goal (theory "LK") "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))";
by (fast_tac LK_pack 1);
-result();
+result();
writeln"Solving for a Var";
-goal LK.thy
+goal (theory "LK")
"|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
by (fast_tac LK_pack 1);
result();
writeln"Principia Mathematica *11.53";
-goal LK.thy
+goal (theory "LK")
"|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
by (fast_tac LK_pack 1);
result();
writeln"Principia Mathematica *11.55";
-goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
+goal (theory "LK") "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
by (fast_tac LK_pack 1);
result();
writeln"Principia Mathematica *11.61";
-goal LK.thy
+goal (theory "LK")
"|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
by (fast_tac LK_pack 1);
result();
-writeln"Reached end of file.";
-
(*21 August 88: loaded in 45.7 secs*)
+(*18 September 2005: loaded in 0.114 secs*)
--- a/src/Sequents/LK0.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK0.ML Sun Sep 18 15:20:08 2005 +0200
@@ -1,9 +1,9 @@
-(* Title: LK/LK0
+(* Title: LK/LK0.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Tactics and lemmas for LK (thanks also to Philippe de Groote)
+Tactics and lemmas for LK (thanks also to Philippe de Groote)
Structural rules by Soren Heilmann
*)
@@ -41,21 +41,21 @@
qed "exchL";
(*Cut and thin, replacing the right-side formula*)
-fun cutR_tac (sP: string) i =
+fun cutR_tac (sP: string) i =
res_inst_tac [ ("P",sP) ] cut i THEN rtac thinR i;
(*Cut and thin, replacing the left-side formula*)
-fun cutL_tac (sP: string) i =
+fun cutL_tac (sP: string) i =
res_inst_tac [ ("P",sP) ] cut i THEN rtac thinL (i+1);
(** If-and-only-if rules **)
-Goalw [iff_def]
+Goalw [iff_def]
"[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F";
by (REPEAT (ares_tac [conjR,impR] 1));
qed "iffR";
-Goalw [iff_def]
+Goalw [iff_def]
"[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E";
by (REPEAT (ares_tac [conjL,impL,basic] 1));
qed "iffL";
@@ -93,31 +93,31 @@
(*The rules of LK*)
-val prop_pack = empty_pack add_safes
- [basic, refl, TrueR, FalseL,
- conjL, conjR, disjL, disjR, impL, impR,
+val prop_pack = empty_pack add_safes
+ [basic, refl, TrueR, FalseL,
+ conjL, conjR, disjL, disjR, impL, impR,
notL, notR, iffL, iffR];
-val LK_pack = prop_pack add_safes [allR, exL]
+val LK_pack = prop_pack add_safes [allR, exL]
add_unsafes [allL_thin, exR_thin, the_equality];
-val LK_dup_pack = prop_pack add_safes [allR, exL]
+val LK_dup_pack = prop_pack add_safes [allR, exL]
add_unsafes [allL, exR, the_equality];
pack_ref() := LK_pack;
-fun lemma_tac th i =
+fun lemma_tac th i =
rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
-val [major,minor] = goal thy
+val [major,minor] = goal (the_context ())
"[| $H |- $E, $F, P --> Q; $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
by (rtac (thinRS RS cut) 1 THEN rtac major 1);
by (Step_tac 1);
by (rtac thinR 1 THEN rtac minor 1);
qed "mp_R";
-val [major,minor] = goal thy
+val [major,minor] = goal (the_context ())
"[| $H, $G |- $E, P --> Q; $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
by (rtac (thinL RS cut) 1 THEN rtac major 1);
by (Step_tac 1);
@@ -127,14 +127,14 @@
(** Two rules to generate left- and right- rules from implications **)
-val [major,minor] = goal thy
+val [major,minor] = goal (the_context ())
"[| |- P --> Q; $H |- $E, $F, P |] ==> $H |- $E, Q, $F";
by (rtac mp_R 1);
by (rtac minor 2);
by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);
qed "R_of_imp";
-val [major,minor] = goal thy
+val [major,minor] = goal (the_context ())
"[| |- P --> Q; $H, $G, Q |- $E |] ==> $H, P, $G |- $E";
by (rtac mp_L 1);
by (rtac minor 2);
@@ -142,7 +142,7 @@
qed "L_of_imp";
(*Can be used to create implications in a subgoal*)
-val [prem] = goal thy
+val [prem] = goal (the_context ())
"[| $H, $G |- $E, $F, P --> Q |] ==> $H, P, $G |- $E, Q, $F";
by (rtac mp_L 1);
by (rtac basic 2);
@@ -151,17 +151,17 @@
Goal "|-P&Q ==> |-P";
by (etac (thinR RS cut) 1);
-by (Fast_tac 1);
+by (Fast_tac 1);
qed "conjunct1";
Goal "|-P&Q ==> |-Q";
by (etac (thinR RS cut) 1);
-by (Fast_tac 1);
+by (Fast_tac 1);
qed "conjunct2";
Goal "|- (ALL x. P(x)) ==> |- P(x)";
by (etac (thinR RS cut) 1);
-by (Fast_tac 1);
+by (Fast_tac 1);
qed "spec";
(** Equality **)
@@ -189,12 +189,12 @@
(* Two theorms for rewriting only one instance of a definition:
the first for definitions of formulae and the second for terms *)
-val prems = goal thy "(A == B) ==> |- A <-> B";
+val prems = goal (the_context ()) "(A == B) ==> |- A <-> B";
by (rewrite_goals_tac prems);
by (rtac iff_refl 1);
qed "def_imp_iff";
-val prems = goal thy "(A == B) ==> |- A = B";
+val prems = goal (the_context ()) "(A == B) ==> |- A = B";
by (rewrite_goals_tac prems);
by (rtac refl 1);
qed "meta_eq_to_obj_eq";
--- a/src/Sequents/LK0.thy Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/LK0.thy Sun Sep 18 15:20:08 2005 +0200
@@ -1,136 +1,139 @@
-(* Title: LK/LK0
+(* Title: LK/LK0.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Classical First-Order Sequent Calculus
-
There may be printing problems if a seqent is in expanded normal form
- (eta-expanded, beta-contracted)
+ (eta-expanded, beta-contracted)
*)
-LK0 = Sequents +
+header {* Classical First-Order Sequent Calculus *}
+
+theory LK0
+imports Sequents
+begin
global
-classes term
-default term
+classes "term"
+defaultsort "term"
consts
- Trueprop :: "two_seqi"
+ Trueprop :: "two_seqi"
- True,False :: o
- "=" :: ['a,'a] => o (infixl 50)
- Not :: o => o ("~ _" [40] 40)
- "&" :: [o,o] => o (infixr 35)
- "|" :: [o,o] => o (infixr 30)
- "-->","<->" :: [o,o] => o (infixr 25)
- The :: ('a => o) => 'a (binder "THE " 10)
- All :: ('a => o) => o (binder "ALL " 10)
- Ex :: ('a => o) => o (binder "EX " 10)
+ True :: o
+ False :: o
+ "=" :: "['a,'a] => o" (infixl 50)
+ Not :: "o => o" ("~ _" [40] 40)
+ "&" :: "[o,o] => o" (infixr 35)
+ "|" :: "[o,o] => o" (infixr 30)
+ "-->" :: "[o,o] => o" (infixr 25)
+ "<->" :: "[o,o] => o" (infixr 25)
+ The :: "('a => o) => 'a" (binder "THE " 10)
+ All :: "('a => o) => o" (binder "ALL " 10)
+ Ex :: "('a => o) => o" (binder "EX " 10)
syntax
- "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
- "_not_equal" :: ['a, 'a] => o (infixl "~=" 50)
+ "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
+ "_not_equal" :: "['a, 'a] => o" (infixl "~=" 50)
+
+parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
+print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
translations
"x ~= y" == "~ (x = y)"
syntax (xsymbols)
- Not :: o => o ("\\<not> _" [40] 40)
- "op &" :: [o, o] => o (infixr "\\<and>" 35)
- "op |" :: [o, o] => o (infixr "\\<or>" 30)
- "op -->" :: [o, o] => o (infixr "\\<longrightarrow>" 25)
- "op <->" :: [o, o] => o (infixr "\\<longleftrightarrow>" 25)
- "ALL " :: [idts, o] => o ("(3\\<forall>_./ _)" [0, 10] 10)
- "EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10)
- "EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10)
- "_not_equal" :: ['a, 'a] => o (infixl "\\<noteq>" 50)
+ Not :: "o => o" ("\<not> _" [40] 40)
+ "op &" :: "[o, o] => o" (infixr "\<and>" 35)
+ "op |" :: "[o, o] => o" (infixr "\<or>" 30)
+ "op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
+ "op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25)
+ "ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
+ "EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
+ "EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10)
+ "_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50)
syntax (HTML output)
- Not :: o => o ("\\<not> _" [40] 40)
- "op &" :: [o, o] => o (infixr "\\<and>" 35)
- "op |" :: [o, o] => o (infixr "\\<or>" 30)
- "ALL " :: [idts, o] => o ("(3\\<forall>_./ _)" [0, 10] 10)
- "EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10)
- "EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10)
- "_not_equal" :: ['a, 'a] => o (infixl "\\<noteq>" 50)
-
+ Not :: "o => o" ("\<not> _" [40] 40)
+ "op &" :: "[o, o] => o" (infixr "\<and>" 35)
+ "op |" :: "[o, o] => o" (infixr "\<or>" 30)
+ "ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
+ "EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
+ "EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10)
+ "_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50)
local
-
-rules
+
+axioms
(*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"
+ contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E"
- thinRS "$H |- $E, $F ==> $H |- $E, $S, $F"
- thinLS "$H, $G |- $E ==> $H, $S, $G |- $E"
+ thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F"
+ thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E"
- 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"
+ exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E"
- cut "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E"
+ cut: "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E"
(*Propositional rules*)
- basic "$H, P, $G |- $E, P, $F"
+ basic: "$H, P, $G |- $E, P, $F"
- 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"
+ conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
- 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"
+ disjL: "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
- 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"
+ impL: "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
- 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"
+ notL: "$H, $G |- $E, P ==> $H, ~P, $G |- $E"
- FalseL "$H, False, $G |- $E"
+ FalseL: "$H, False, $G |- $E"
- True_def "True == False-->False"
- iff_def "P<->Q == (P-->Q) & (Q-->P)"
+ True_def: "True == False-->False"
+ iff_def: "P<->Q == (P-->Q) & (Q-->P)"
(*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"
+ allL: "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
- 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"
+ exL: "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
(*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"
+ subst: "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
(* Reflection *)
- eq_reflection "|- x=y ==> (x==y)"
- iff_reflection "|- P<->Q ==> (P==Q)"
+ eq_reflection: "|- x=y ==> (x==y)"
+ iff_reflection: "|- P<->Q ==> (P==Q)"
(*Descriptions*)
- The "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==>
+ The: "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==>
$H |- $E, P(THE x. P(x)), $F"
constdefs
- If :: [o, 'a, 'a] => 'a ("(if (_)/ then (_)/ else (_))" 10)
+ If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
"If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
setup
prover_setup
+ML {* use_legacy_bindings (the_context ()) *}
+
end
-ML
-
-val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
-val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
-
--- a/src/Sequents/Modal/ROOT.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/Modal/ROOT.ML Sun Sep 18 15:20:08 2005 +0200
@@ -1,21 +1,21 @@
-(* Title: Modal/ex/ROOT
+(* Title: Modal/ex/ROOT.ML
ID: $Id$
Author: Martin Coen
Copyright 1991 University of Cambridge
*)
writeln "\nTheorems of T\n";
-fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
+fun try s = (writeln s; prove_goal (theory "T") s (fn _=> [T_Prover.solve_tac 2]));
time_use "Tthms.ML";
writeln "\nTheorems of S4\n";
-fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2]));
+fun try s = (writeln s; prove_goal (theory "S4") s (fn _=> [S4_Prover.solve_tac 2]));
time_use "Tthms.ML";
time_use "S4thms.ML";
writeln "\nTheorems of S43\n";
fun try s = (writeln s;
- prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE
+ prove_goal (theory "S43") s (fn _=> [S43_Prover.solve_tac 2 ORELSE
S43_Prover.solve_tac 3]));
time_use "Tthms.ML";
time_use "S4thms.ML";
--- a/src/Sequents/Modal0.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/Modal0.ML Sun Sep 18 15:20:08 2005 +0200
@@ -4,19 +4,19 @@
Copyright 1991 University of Cambridge
*)
-structure Modal0_rls =
+structure Modal0_rls =
struct
-val rewrite_rls = [Modal0.strimp_def,Modal0.streqv_def];
+val rewrite_rls = [strimp_def,streqv_def];
local
- val iffR = prove_goal thy
+ val iffR = prove_goal (the_context ())
"[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
(fn prems=>
[ (rewtac iff_def),
(REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
- val iffL = prove_goal thy
+ val iffL = prove_goal (the_context ())
"[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
(fn prems=>
[ rewtac iff_def,
--- a/src/Sequents/Modal0.thy Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/Modal0.thy Sun Sep 18 15:20:08 2005 +0200
@@ -1,42 +1,43 @@
-(* Title: Sequents/Modal0
+(* Title: Sequents/Modal0.thy
ID: $Id$
Author: Martin Coen
Copyright 1991 University of Cambridge
*)
-Modal0 = LK0 +
+theory Modal0
+imports LK0
+uses "modal.ML"
+begin
consts
box :: "o=>o" ("[]_" [50] 50)
dia :: "o=>o" ("<>_" [50] 50)
- "--<",">-<" :: "[o,o]=>o" (infixr 25)
- Lstar,Rstar :: "two_seqi"
+ "--<" :: "[o,o]=>o" (infixr 25)
+ ">-<" :: "[o,o]=>o" (infixr 25)
+ Lstar :: "two_seqi"
+ Rstar :: "two_seqi"
syntax
"@Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5)
"@Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5)
-rules
- (* Definitions *)
-
- strimp_def "P --< Q == [](P --> Q)"
- streqv_def "P >-< Q == (P --< Q) & (Q --< P)"
-end
-
-ML
-
-local
-
+ML {*
val Lstar = "Lstar";
val Rstar = "Rstar";
val SLstar = "@Lstar";
val SRstar = "@Rstar";
- fun star_tr c [s1,s2] =
- Const(c,dummyT)$Sequents.seq_tr s1$Sequents.seq_tr s2;
- fun star_tr' c [s1,s2] =
- Const(c,dummyT) $ Sequents.seq_tr' s1 $ Sequents.seq_tr' s2;
-in
-val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
-val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
-end;
+ fun star_tr c [s1,s2] = Const(c,dummyT)$ seq_tr s1$ seq_tr s2;
+ fun star_tr' c [s1,s2] = Const(c,dummyT) $ seq_tr' s1 $ seq_tr' s2;
+*}
+
+parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
+print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
+
+defs
+ strimp_def: "P --< Q == [](P --> Q)"
+ streqv_def: "P >-< Q == (P --< Q) & (Q --< P)"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
+end
--- a/src/Sequents/ROOT.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/ROOT.ML Sun Sep 18 15:20:08 2005 +0200
@@ -3,29 +3,18 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-Adds Classical Sequent Calculus to a database containing pure Isabelle.
+Classical Sequent Calculus based on Pure Isabelle.
*)
val banner = "Sequent Calculii";
writeln banner;
-print_depth 1;
-
Unify.trace_bound:= 20;
Unify.search_bound := 40;
-use_thy "Sequents";
-use "prover.ML";
-
use_thy "LK";
-use "simpdata.ML";
-
use_thy "ILL";
-
-use "modal.ML";
use_thy "Modal0";
use_thy"T";
use_thy"S4";
use_thy"S43";
-
-print_depth 8;
--- a/src/Sequents/S4.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/S4.ML Sun Sep 18 15:20:08 2005 +0200
@@ -1,10 +1,10 @@
-(* Title: Modal/S4
+(* Title: Modal/S4.ML
ID: $Id$
Author: Martin Coen
Copyright 1991 University of Cambridge
*)
-local open Modal0_rls S4
+local open Modal0_rls
in structure MP_Rule : MODAL_PROVER_RULE =
struct
val rewrite_rls = rewrite_rls
--- a/src/Sequents/S4.thy Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/S4.thy Sun Sep 18 15:20:08 2005 +0200
@@ -1,31 +1,37 @@
-(* Title: Modal/S4
+(* Title: Modal/S4.thy
ID: $Id$
Author: Martin Coen
Copyright 1991 University of Cambridge
*)
-S4 = Modal0 +
-rules
+theory S4
+imports Modal0
+begin
+
+axioms
(* 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>"
+ 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"
(* Rules for [] and <> *)
- boxR
- "[| $E |L> $E'; $F |R> $F'; $G |R> $G';
+ 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"
+ boxL: "$E,P,$F,[]P |- $G ==> $E, []P, $F |- $G"
- diaR "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G"
- diaL
- "[| $E |L> $E'; $F |L> $F'; $G |R> $G';
+ diaR: "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G"
+ diaL:
+ "[| $E |L> $E'; $F |L> $F'; $G |R> $G';
$E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/Sequents/S43.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/S43.ML Sun Sep 18 15:20:08 2005 +0200
@@ -2,11 +2,9 @@
ID: $Id$
Author: Martin Coen
Copyright 1991 University of Cambridge
-
-This implements Rajeev Gore's sequent calculus for S43.
*)
-local open Modal0_rls S43
+local open Modal0_rls
in structure MP_Rule : MODAL_PROVER_RULE =
struct
val rewrite_rls = rewrite_rls
@@ -16,4 +14,4 @@
val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2,S43pi0,S43pi1,S43pi2]
end;
end;
-structure S43_Prover = Modal_ProverFun(MP_Rule);
+structure S43_Prover = Modal_ProverFun(MP_Rule);
--- a/src/Sequents/S43.thy Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/S43.thy Sun Sep 18 15:20:08 2005 +0200
@@ -1,4 +1,4 @@
-(* Title: Modal/S43
+(* Title: Modal/S43.thy
ID: $Id$
Author: Martin Coen
Copyright 1991 University of Cambridge
@@ -6,7 +6,9 @@
This implements Rajeev Gore's sequent calculus for S43.
*)
-S43 = Modal0 +
+theory S43
+imports Modal0
+begin
consts
S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
@@ -15,17 +17,34 @@
"@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
-rules
+ML {*
+ val S43pi = "S43pi";
+ val SS43pi = "@S43pi";
+
+ val tr = seq_tr;
+ val tr' = seq_tr';
+
+ fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
+ Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
+ fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
+ Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
+
+*}
+
+parse_translation {* [(SS43pi,s43pi_tr)] *}
+print_translation {* [(S43pi,s43pi_tr')] *}
+
+axioms
(* 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>"
+ 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"
(* Set of Horn clauses to generate the antecedents for the S43 pi rule *)
(* ie *)
@@ -37,43 +56,27 @@
(* 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"
- S43pi1
- "[| (S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox |- $R,$Rdia |] ==>
+ S43pi0: "S43pi $L;; $R;; $Lbox; $Rdia"
+ S43pi1:
+ "[| (S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox |- $R,$Rdia |] ==>
S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia"
- S43pi2
- "[| (S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox |- $R',P,$R,$Rdia |] ==>
+ S43pi2:
+ "[| (S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox |- $R',P,$R,$Rdia |] ==>
S43pi $L';; $R'; []P,$R; $Lbox;$Rdia"
(* 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"
- pi1
- "[| $L1,<>P,$L2 |L> $Lbox; $L1,<>P,$L2 |R> $Ldia; $R |L> $Rbox; $R |R> $Rdia;
- S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
+ boxL: "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
+ diaR: "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
+ 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"
- pi2
- "[| $L |L> $Lbox; $L |R> $Ldia; $R1,[]P,$R2 |L> $Rbox; $R1,[]P,$R2 |R> $Rdia;
- S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
+ pi2:
+ "[| $L |L> $Lbox; $L |R> $Ldia; $R1,[]P,$R2 |L> $Rbox; $R1,[]P,$R2 |R> $Rdia;
+ S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
$L |- $R1, []P, $R2"
-end
-
-ML
-local
-
- val S43pi = "S43pi";
- val SS43pi = "@S43pi";
-
- val tr = Sequents.seq_tr;
- val tr' = Sequents.seq_tr';
+ML {* use_legacy_bindings (the_context ()) *}
- fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
- Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
- fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
- Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
-in
-val parse_translation = [(SS43pi,s43pi_tr)];
-val print_translation = [(S43pi,s43pi_tr')]
end
--- a/src/Sequents/Sequents.thy Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/Sequents.thy Sun Sep 18 15:20:08 2005 +0200
@@ -1,29 +1,29 @@
-(* Title: Sequents/Sequents.thy
+(* Title: Sequents/Sequents.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-
-Basis theory for parsing and pretty-printing of sequences to be used in
-Sequent Calculi.
*)
-Sequents = Pure +
+header {* Parsing and pretty-printing of sequences *}
+
+theory Sequents
+imports Pure
+uses ("prover.ML")
+begin
global
-types
- o
-
+typedecl o
(* Sequences *)
-types
+typedecl
seq'
consts
- SeqO' :: [o,seq']=>seq'
- Seq1' :: o=>seq'
-
+ SeqO' :: "[o,seq']=>seq'"
+ Seq1' :: "o=>seq'"
+
(* concrete syntax *)
@@ -32,37 +32,33 @@
syntax
- SeqEmp :: seq ("")
- SeqApp :: [seqobj,seqcont] => seq ("__")
+ SeqEmp :: seq ("")
+ SeqApp :: "[seqobj,seqcont] => seq" ("__")
- SeqContEmp :: seqcont ("")
- SeqContApp :: [seqobj,seqcont] => seqcont (",/ __")
-
- SeqO :: o => seqobj ("_")
- SeqId :: 'a => seqobj ("$_")
+ SeqContEmp :: seqcont ("")
+ SeqContApp :: "[seqobj,seqcont] => seqcont" (",/ __")
+
+ SeqO :: "o => seqobj" ("_")
+ SeqId :: "'a => seqobj" ("$_")
types
-
- single_seqe = [seq,seqobj] => prop
- single_seqi = [seq'=>seq',seq'=>seq'] => prop
- two_seqi = [seq'=>seq', seq'=>seq'] => prop
- two_seqe = [seq, seq] => prop
- three_seqi = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop
- three_seqe = [seq, seq, seq] => prop
- four_seqi = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop
- four_seqe = [seq, seq, seq, seq] => prop
+ single_seqe = "[seq,seqobj] => prop"
+ single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
+ two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
+ two_seqe = "[seq, seq] => prop"
+ three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+ three_seqe = "[seq, seq, seq] => prop"
+ four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+ four_seqe = "[seq, seq, seq, seq] => prop"
-
- sequence_name = seq'=>seq'
+ sequence_name = "seq'=>seq'"
syntax
(*Constant to allow definitions of SEQUENCES of formulas*)
- "@Side" :: seq=>(seq'=>seq') ("<<(_)>>")
+ "@Side" :: "seq=>(seq'=>seq')" ("<<(_)>>")
-end
-
-ML
+ML {*
(* parse translation for sequences *)
@@ -70,49 +66,49 @@
fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f |
seqobj_tr(_ $ i) = i;
-
+
fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 |
- seqcont_tr(Const("SeqContApp",_) $ so $ sc) =
+ seqcont_tr(Const("SeqContApp",_) $ so $ sc) =
(seqobj_tr so) $ (seqcont_tr sc);
fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) |
- seq_tr(Const("SeqApp",_) $ so $ sc) =
+ seq_tr(Const("SeqApp",_) $ so $ sc) =
abs_seq'(seqobj_tr(so) $ seqcont_tr(sc));
fun singlobj_tr(Const("SeqO",_) $ f) =
abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0);
-
+
-
+
(* print translation for sequences *)
-fun seqcont_tr' (Bound 0) =
+fun seqcont_tr' (Bound 0) =
Const("SeqContEmp",dummyT) |
seqcont_tr' (Const("SeqO'",_) $ f $ s) =
- Const("SeqContApp",dummyT) $
- (Const("SeqO",dummyT) $ f) $
+ Const("SeqContApp",dummyT) $
+ (Const("SeqO",dummyT) $ f) $
(seqcont_tr' s) |
-(* seqcont_tr' ((a as Abs(_,_,_)) $ s)=
+(* seqcont_tr' ((a as Abs(_,_,_)) $ s)=
seqcont_tr'(betapply(a,s)) | *)
- seqcont_tr' (i $ s) =
- Const("SeqContApp",dummyT) $
- (Const("SeqId",dummyT) $ i) $
+ seqcont_tr' (i $ s) =
+ Const("SeqContApp",dummyT) $
+ (Const("SeqId",dummyT) $ i) $
(seqcont_tr' s);
fun seq_tr' s =
- let fun seq_itr' (Bound 0) =
+ let fun seq_itr' (Bound 0) =
Const("SeqEmp",dummyT) |
seq_itr' (Const("SeqO'",_) $ f $ s) =
- Const("SeqApp",dummyT) $
+ Const("SeqApp",dummyT) $
(Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) |
(* seq_itr' ((a as Abs(_,_,_)) $ s) =
seq_itr'(betapply(a,s)) | *)
seq_itr' (i $ s) =
- Const("SeqApp",dummyT) $
- (Const("SeqId",dummyT) $ i) $
+ Const("SeqApp",dummyT) $
+ (Const("SeqId",dummyT) $ i) $
(seqcont_tr' s)
- in case s of
+ in case s of
Abs(_,_,t) => seq_itr' t |
_ => s $ (Bound 0)
end;
@@ -138,22 +134,28 @@
fun single_tr' c [s1, s2] =
-(Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 );
+(Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 );
fun two_seq_tr' c [s1, s2] =
- Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
+ Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
fun three_seq_tr' c [s1, s2, s3] =
- Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;
+ Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3;
fun four_seq_tr' c [s1, s2, s3, s4] =
- Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;
+ Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 $ seq_tr' s3 $ seq_tr' s4;
+
-
(** for the <<...>> notation **)
-
+
fun side_tr [s1] = seq_tr s1;
+*}
-val parse_translation = [("@Side", side_tr)];
+parse_translation {* [("@Side", side_tr)] *}
+
+use "prover.ML"
+
+end
+
--- a/src/Sequents/T.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/T.ML Sun Sep 18 15:20:08 2005 +0200
@@ -1,10 +1,10 @@
-(* Title: Modal/T
+(* Title: Modal/T.ML
ID: $Id$
Author: Martin Coen
Copyright 1991 University of Cambridge
*)
-local open Modal0_rls T
+local open Modal0_rls
in structure MP_Rule : MODAL_PROVER_RULE =
struct
val rewrite_rls = rewrite_rls
@@ -14,4 +14,4 @@
val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2]
end
end;
-structure T_Prover = Modal_ProverFun(MP_Rule);
+structure T_Prover = Modal_ProverFun(MP_Rule);
--- a/src/Sequents/T.thy Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/T.thy Sun Sep 18 15:20:08 2005 +0200
@@ -1,30 +1,36 @@
-(* Title: Modal/T
+(* Title: Modal/T.thy
ID: $Id$
Author: Martin Coen
Copyright 1991 University of Cambridge
*)
-T = Modal0 +
-rules
+theory T
+imports Modal0
+begin
+
+axioms
(* 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>"
+ 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"
(* Rules for [] and <> *)
- boxR
- "[| $E |L> $E'; $F |R> $F'; $G |R> $G';
+ 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"
- diaL
- "[| $E |L> $E'; $F |L> $F'; $G |R> $G';
+ boxL: "$E, P, $F |- $G ==> $E, []P, $F |- $G"
+ diaR: "$E |- $F, P, $G ==> $E |- $F, <>P, $G"
+ diaL:
+ "[| $E |L> $E'; $F |L> $F'; $G |R> $G';
$E', P, $F'|- $G'|] ==> $E, <>P, $F |- $G"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end
--- a/src/Sequents/simpdata.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/simpdata.ML Sun Sep 18 15:20:08 2005 +0200
@@ -12,7 +12,7 @@
fun prove_fun s =
(writeln s;
- prove_goal LK.thy s
+ prove_goal (the_context ()) s
(fn prems => [ (cut_facts_tac prems 1),
(fast_tac (pack() add_safes [subst]) 1) ]));
@@ -144,7 +144,7 @@
(*** Named rewrite rules ***)
-fun prove nm thm = qed_goal nm LK.thy thm
+fun prove nm thm = qed_goal nm (the_context ()) thm
(fn prems => [ (cut_facts_tac prems 1),
(fast_tac LK_pack 1) ]);
@@ -264,7 +264,7 @@
(* To create substition rules *)
-qed_goal "eq_imp_subst" LK.thy "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
+qed_goal "eq_imp_subst" (the_context ()) "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
(fn prems =>
[cut_facts_tac prems 1,
asm_simp_tac LK_basic_ss 1]);