--- a/src/Sequents/ILL.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/ILL.thy Sat Oct 10 20:51:39 2015 +0200
@@ -10,16 +10,16 @@
consts
Trueprop :: "two_seqi"
- tens :: "[o, o] => o" (infixr "><" 35)
- limp :: "[o, o] => o" (infixr "-o" 45)
- liff :: "[o, o] => o" (infixr "o-o" 45)
- FShriek :: "o => o" ("! _" [100] 1000)
- lconj :: "[o, o] => o" (infixr "&&" 35)
- ldisj :: "[o, o] => o" (infixr "++" 35)
+ tens :: "[o, o] \<Rightarrow> o" (infixr "><" 35)
+ limp :: "[o, o] \<Rightarrow> o" (infixr "-o" 45)
+ liff :: "[o, o] \<Rightarrow> o" (infixr "o-o" 45)
+ FShriek :: "o \<Rightarrow> o" ("! _" [100] 1000)
+ lconj :: "[o, o] \<Rightarrow> o" (infixr "&&" 35)
+ ldisj :: "[o, o] \<Rightarrow> o" (infixr "++" 35)
zero :: "o" ("0")
top :: "o" ("1")
eye :: "o" ("I")
- aneg :: "o=>o" ("~_")
+ aneg :: "o\<Rightarrow>o" ("~_")
(* context manipulation *)
@@ -62,67 +62,67 @@
(* RULES THAT DO NOT DIVIDE CONTEXT *)
-derelict: "$F, A, $G |- C ==> $F, !A, $G |- C" and
+derelict: "$F, A, $G |- C \<Longrightarrow> $F, !A, $G |- C" and
(* unfortunately, this one removes !A *)
-contract: "$F, !A, !A, $G |- C ==> $F, !A, $G |- C" and
+contract: "$F, !A, !A, $G |- C \<Longrightarrow> $F, !A, $G |- C" and
-weaken: "$F, $G |- C ==> $G, !A, $F |- C" and
+weaken: "$F, $G |- C \<Longrightarrow> $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" and
+promote2: "promaux{ || $H || B} \<Longrightarrow> $H |- !B" and
promote1: "promaux{!A, $G || $H || B}
- ==> promaux {$G || $H, !A || B}" and
-promote0: "$G |- A ==> promaux {$G || || A}" and
+ \<Longrightarrow> promaux {$G || $H, !A || B}" and
+promote0: "$G |- A \<Longrightarrow> promaux {$G || || A}" and
-tensl: "$H, A, B, $G |- C ==> $H, A >< B, $G |- C" and
+tensl: "$H, A, B, $G |- C \<Longrightarrow> $H, A >< B, $G |- C" and
-impr: "A, $F |- B ==> $F |- A -o B" and
+impr: "A, $F |- B \<Longrightarrow> $F |- A -o B" and
-conjr: "[| $F |- A ;
- $F |- B |]
- ==> $F |- (A && B)" and
+conjr: "\<lbrakk>$F |- A ;
+ $F |- B\<rbrakk>
+ \<Longrightarrow> $F |- (A && B)" and
-conjll: "$G, A, $H |- C ==> $G, A && B, $H |- C" and
+conjll: "$G, A, $H |- C \<Longrightarrow> $G, A && B, $H |- C" and
-conjlr: "$G, B, $H |- C ==> $G, A && B, $H |- C" and
+conjlr: "$G, B, $H |- C \<Longrightarrow> $G, A && B, $H |- C" and
-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" and
+disjrl: "$G |- A \<Longrightarrow> $G |- A ++ B" and
+disjrr: "$G |- B \<Longrightarrow> $G |- A ++ B" and
+disjl: "\<lbrakk>$G, A, $H |- C ;
+ $G, B, $H |- C\<rbrakk>
+ \<Longrightarrow> $G, A ++ B, $H |- C" and
(* RULES THAT DIVIDE CONTEXT *)
-tensr: "[| $F, $J :=: $G;
- $F |- A ;
- $J |- B |]
- ==> $G |- A >< B" and
+tensr: "\<lbrakk>$F, $J :=: $G;
+ $F |- A ;
+ $J |- B\<rbrakk>
+ \<Longrightarrow> $G |- A >< B" and
-impl: "[| $G, $F :=: $J, $H ;
- B, $F |- C ;
- $G |- A |]
- ==> $J, A -o B, $H |- C" and
+impl: "\<lbrakk>$G, $F :=: $J, $H ;
+ B, $F |- C ;
+ $G |- A\<rbrakk>
+ \<Longrightarrow> $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" and
+cut: "\<lbrakk> $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
+ $H1, $H2, $H3, $H4 |- A ;
+ $J1, $J2, A, $J3, $J4 |- B\<rbrakk> \<Longrightarrow> $F |- B" and
(* CONTEXT RULES *)
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"
+context2: "$F, $G :=: $H, !A, $G \<Longrightarrow> $F, A, $G :=: $H, !A, $G" and
+context3: "$F, $G :=: $H, $J \<Longrightarrow> $F, A, $G :=: $H, A, $J" and
+context4a: "$F :=: $H, $G \<Longrightarrow> $F :=: $H, !A, $G" and
+context4b: "$F, $H :=: $G \<Longrightarrow> $F, !A, $H :=: $G" and
+context5: "$F, $G :=: $H \<Longrightarrow> $G, $F :=: $H"
text "declarations for lazy classical reasoning:"
lemmas [safe] =
--- a/src/Sequents/ILL_predlog.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/ILL_predlog.thy Sat Oct 10 20:51:39 2015 +0200
@@ -5,26 +5,25 @@
typedecl plf
consts
- conj :: "[plf,plf] => plf" (infixr "&" 35)
- disj :: "[plf,plf] => plf" (infixr "|" 35)
- impl :: "[plf,plf] => plf" (infixr ">" 35)
- eq :: "[plf,plf] => plf" (infixr "=" 35)
+ conj :: "[plf,plf] \<Rightarrow> plf" (infixr "&" 35)
+ disj :: "[plf,plf] \<Rightarrow> plf" (infixr "|" 35)
+ impl :: "[plf,plf] \<Rightarrow> plf" (infixr ">" 35)
+ eq :: "[plf,plf] \<Rightarrow> plf" (infixr "=" 35)
ff :: "plf" ("ff")
- PL :: "plf => o" ("[* / _ / *]" [] 100)
+ PL :: "plf \<Rightarrow> o" ("[* / _ / *]" [] 100)
syntax
- "_NG" :: "plf => plf" ("- _ " [50] 55)
+ "_NG" :: "plf \<Rightarrow> plf" ("- _ " [50] 55)
translations
+ "[* A & B *]" \<rightleftharpoons> "[*A*] && [*B*]"
+ "[* A | B *]" \<rightleftharpoons> "![*A*] ++ ![*B*]"
+ "[* - A *]" \<rightleftharpoons> "[*A > ff*]"
+ "[* ff *]" \<rightleftharpoons> "0"
+ "[* A = B *]" \<rightharpoonup> "[* (A > B) & (B > A) *]"
- "[* A & B *]" == "[*A*] && [*B*]"
- "[* A | B *]" == "![*A*] ++ ![*B*]"
- "[* - A *]" == "[*A > ff*]"
- "[* ff *]" == "0"
- "[* A = B *]" => "[* (A > B) & (B > A) *]"
-
- "[* A > B *]" == "![*A*] -o [*B*]"
+ "[* A > B *]" \<rightleftharpoons> "![*A*] -o [*B*]"
(* another translations for linear implication:
"[* A > B *]" == "!([*A*] -o [*B*])" *)
--- a/src/Sequents/LK.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/LK.thy Sat Oct 10 20:51:39 2015 +0200
@@ -3,7 +3,7 @@
Copyright 1993 University of Cambridge
Axiom to express monotonicity (a variant of the deduction theorem). Makes the
-link between |- and ==>, needed for instance to prove imp_cong.
+link between |- and \<Longrightarrow>, needed for instance to prove imp_cong.
Axiom left_cong allows the simplifier to use left-side formulas. Ideally it
should be derived from lower-level axioms.
@@ -17,111 +17,111 @@
begin
axiomatization where
- monotonic: "($H |- P ==> $H |- Q) ==> $H, P |- Q" and
+ monotonic: "($H |- P \<Longrightarrow> $H |- Q) \<Longrightarrow> $H, P |- Q" and
- left_cong: "[| P == P'; |- P' ==> ($H |- $F) == ($H' |- $F') |]
- ==> (P, $H |- $F) == (P', $H' |- $F')"
+ left_cong: "\<lbrakk>P == P'; |- P' \<Longrightarrow> ($H |- $F) \<equiv> ($H' |- $F')\<rbrakk>
+ \<Longrightarrow> (P, $H |- $F) \<equiv> (P', $H' |- $F')"
subsection \<open>Rewrite rules\<close>
lemma conj_simps:
- "|- P & True <-> P"
- "|- True & P <-> P"
- "|- P & False <-> False"
- "|- False & P <-> False"
- "|- P & P <-> P"
- "|- P & P & Q <-> P & Q"
- "|- P & ~P <-> False"
- "|- ~P & P <-> False"
- "|- (P & Q) & R <-> P & (Q & R)"
+ "|- P \<and> True \<longleftrightarrow> P"
+ "|- True \<and> P \<longleftrightarrow> P"
+ "|- P \<and> False \<longleftrightarrow> False"
+ "|- False \<and> P \<longleftrightarrow> False"
+ "|- P \<and> P \<longleftrightarrow> P"
+ "|- P \<and> P \<and> Q \<longleftrightarrow> P \<and> Q"
+ "|- P \<and> \<not> P \<longleftrightarrow> False"
+ "|- \<not> P \<and> P \<longleftrightarrow> False"
+ "|- (P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
by (fast add!: subst)+
lemma disj_simps:
- "|- P | True <-> True"
- "|- True | P <-> True"
- "|- P | False <-> P"
- "|- False | P <-> P"
- "|- P | P <-> P"
- "|- P | P | Q <-> P | Q"
- "|- (P | Q) | R <-> P | (Q | R)"
+ "|- P \<or> True \<longleftrightarrow> True"
+ "|- True \<or> P \<longleftrightarrow> True"
+ "|- P \<or> False \<longleftrightarrow> P"
+ "|- False \<or> P \<longleftrightarrow> P"
+ "|- P \<or> P \<longleftrightarrow> P"
+ "|- P \<or> P \<or> Q \<longleftrightarrow> P \<or> Q"
+ "|- (P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
by (fast add!: subst)+
lemma not_simps:
- "|- ~ False <-> True"
- "|- ~ True <-> False"
+ "|- \<not> False \<longleftrightarrow> True"
+ "|- \<not> True \<longleftrightarrow> False"
by (fast add!: subst)+
lemma imp_simps:
- "|- (P --> False) <-> ~P"
- "|- (P --> True) <-> True"
- "|- (False --> P) <-> True"
- "|- (True --> P) <-> P"
- "|- (P --> P) <-> True"
- "|- (P --> ~P) <-> ~P"
+ "|- (P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
+ "|- (P \<longrightarrow> True) \<longleftrightarrow> True"
+ "|- (False \<longrightarrow> P) \<longleftrightarrow> True"
+ "|- (True \<longrightarrow> P) \<longleftrightarrow> P"
+ "|- (P \<longrightarrow> P) \<longleftrightarrow> True"
+ "|- (P \<longrightarrow> \<not> P) \<longleftrightarrow> \<not> P"
by (fast add!: subst)+
lemma iff_simps:
- "|- (True <-> P) <-> P"
- "|- (P <-> True) <-> P"
- "|- (P <-> P) <-> True"
- "|- (False <-> P) <-> ~P"
- "|- (P <-> False) <-> ~P"
+ "|- (True \<longleftrightarrow> P) \<longleftrightarrow> P"
+ "|- (P \<longleftrightarrow> True) \<longleftrightarrow> P"
+ "|- (P \<longleftrightarrow> P) \<longleftrightarrow> True"
+ "|- (False \<longleftrightarrow> P) \<longleftrightarrow> \<not> P"
+ "|- (P \<longleftrightarrow> False) \<longleftrightarrow> \<not> P"
by (fast add!: subst)+
lemma quant_simps:
- "!!P. |- (ALL x. P) <-> P"
- "!!P. |- (ALL x. x=t --> P(x)) <-> P(t)"
- "!!P. |- (ALL x. t=x --> P(x)) <-> P(t)"
- "!!P. |- (EX x. P) <-> P"
- "!!P. |- (EX x. x=t & P(x)) <-> P(t)"
- "!!P. |- (EX x. t=x & P(x)) <-> P(t)"
+ "\<And>P. |- (\<forall>x. P) \<longleftrightarrow> P"
+ "\<And>P. |- (\<forall>x. x = t \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
+ "\<And>P. |- (\<forall>x. t = x \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
+ "\<And>P. |- (\<exists>x. P) \<longleftrightarrow> P"
+ "\<And>P. |- (\<exists>x. x = t \<and> P(x)) \<longleftrightarrow> P(t)"
+ "\<And>P. |- (\<exists>x. t = x \<and> P(x)) \<longleftrightarrow> P(t)"
by (fast add!: subst)+
subsection \<open>Miniscoping: pushing quantifiers in\<close>
text \<open>
- We do NOT distribute of ALL over &, or dually that of EX over |
+ We do NOT distribute of \<forall> over \<and>, or dually that of \<exists> over \<or>
Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
show that this step can increase proof length!
\<close>
text \<open>existential miniscoping\<close>
lemma ex_simps:
- "!!P Q. |- (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
- "!!P Q. |- (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
- "!!P Q. |- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
- "!!P Q. |- (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
- "!!P Q. |- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q"
- "!!P Q. |- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"
+ "\<And>P Q. |- (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
+ "\<And>P Q. |- (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
+ "\<And>P Q. |- (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
+ "\<And>P Q. |- (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
+ "\<And>P Q. |- (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+ "\<And>P Q. |- (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))"
by (fast add!: subst)+
text \<open>universal miniscoping\<close>
lemma all_simps:
- "!!P Q. |- (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
- "!!P Q. |- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
- "!!P Q. |- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q"
- "!!P Q. |- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"
- "!!P Q. |- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
- "!!P Q. |- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
+ "\<And>P Q. |- (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
+ "\<And>P Q. |- (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
+ "\<And>P Q. |- (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<longrightarrow> Q"
+ "\<And>P Q. |- (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))"
+ "\<And>P Q. |- (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
+ "\<And>P Q. |- (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))"
by (fast add!: subst)+
text \<open>These are NOT supplied by default!\<close>
lemma distrib_simps:
- "|- P & (Q | R) <-> P&Q | P&R"
- "|- (Q | R) & P <-> Q&P | R&P"
- "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"
+ "|- P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R"
+ "|- (Q \<or> R) \<and> P \<longleftrightarrow> Q \<and> P \<or> R \<and> P"
+ "|- (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
by (fast add!: subst)+
-lemma P_iff_F: "|- ~P ==> |- (P <-> False)"
+lemma P_iff_F: "|- \<not> P \<Longrightarrow> |- (P \<longleftrightarrow> False)"
apply (erule thinR [THEN cut])
apply fast
done
lemmas iff_reflection_F = P_iff_F [THEN iff_reflection]
-lemma P_iff_T: "|- P ==> |- (P <-> True)"
+lemma P_iff_T: "|- P \<Longrightarrow> |- (P \<longleftrightarrow> True)"
apply (erule thinR [THEN cut])
apply fast
done
@@ -130,51 +130,51 @@
lemma LK_extra_simps:
- "|- P | ~P"
- "|- ~P | P"
- "|- ~ ~ P <-> P"
- "|- (~P --> P) <-> P"
- "|- (~P <-> ~Q) <-> (P<->Q)"
+ "|- P \<or> \<not> P"
+ "|- \<not> P \<or> P"
+ "|- \<not> \<not> P \<longleftrightarrow> P"
+ "|- (\<not> P \<longrightarrow> P) \<longleftrightarrow> P"
+ "|- (\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)"
by (fast add!: subst)+
subsection \<open>Named rewrite rules\<close>
-lemma conj_commute: "|- P&Q <-> Q&P"
- and conj_left_commute: "|- P&(Q&R) <-> Q&(P&R)"
+lemma conj_commute: "|- P \<and> Q \<longleftrightarrow> Q \<and> P"
+ and conj_left_commute: "|- P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)"
by (fast add!: subst)+
lemmas conj_comms = conj_commute conj_left_commute
-lemma disj_commute: "|- P|Q <-> Q|P"
- and disj_left_commute: "|- P|(Q|R) <-> Q|(P|R)"
+lemma disj_commute: "|- P \<or> Q \<longleftrightarrow> Q \<or> P"
+ and disj_left_commute: "|- P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)"
by (fast add!: subst)+
lemmas disj_comms = disj_commute disj_left_commute
-lemma conj_disj_distribL: "|- P&(Q|R) <-> (P&Q | P&R)"
- and conj_disj_distribR: "|- (P|Q)&R <-> (P&R | Q&R)"
+lemma conj_disj_distribL: "|- P \<and> (Q \<or> R) \<longleftrightarrow> (P \<and> Q \<or> P \<and> R)"
+ and conj_disj_distribR: "|- (P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R \<or> Q \<and> R)"
- and disj_conj_distribL: "|- P|(Q&R) <-> (P|Q) & (P|R)"
- and disj_conj_distribR: "|- (P&Q)|R <-> (P|R) & (Q|R)"
+ and disj_conj_distribL: "|- P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
+ and disj_conj_distribR: "|- (P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)"
- and imp_conj_distrib: "|- (P --> (Q&R)) <-> (P-->Q) & (P-->R)"
- and imp_conj: "|- ((P&Q)-->R) <-> (P --> (Q --> R))"
- and imp_disj: "|- (P|Q --> R) <-> (P-->R) & (Q-->R)"
+ and imp_conj_distrib: "|- (P \<longrightarrow> (Q \<and> R)) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
+ and imp_conj: "|- ((P \<and> Q) \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
+ and imp_disj: "|- (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
- and imp_disj1: "|- (P-->Q) | R <-> (P-->Q | R)"
- and imp_disj2: "|- Q | (P-->R) <-> (P-->Q | R)"
+ and imp_disj1: "|- (P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
+ and imp_disj2: "|- Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
- and de_Morgan_disj: "|- (~(P | Q)) <-> (~P & ~Q)"
- and de_Morgan_conj: "|- (~(P & Q)) <-> (~P | ~Q)"
+ and de_Morgan_disj: "|- (\<not> (P \<or> Q)) \<longleftrightarrow> (\<not> P \<and> \<not> Q)"
+ and de_Morgan_conj: "|- (\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)"
- and not_iff: "|- ~(P <-> Q) <-> (P <-> ~Q)"
+ and not_iff: "|- \<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)"
by (fast add!: subst)+
lemma imp_cong:
- assumes p1: "|- P <-> P'"
- and p2: "|- P' ==> |- Q <-> Q'"
- shows "|- (P-->Q) <-> (P'-->Q')"
+ assumes p1: "|- P \<longleftrightarrow> P'"
+ and p2: "|- P' \<Longrightarrow> |- Q \<longleftrightarrow> Q'"
+ shows "|- (P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q')"
apply (lem p1)
apply safe
apply (tactic \<open>
@@ -185,9 +185,9 @@
done
lemma conj_cong:
- assumes p1: "|- P <-> P'"
- and p2: "|- P' ==> |- Q <-> Q'"
- shows "|- (P&Q) <-> (P'&Q')"
+ assumes p1: "|- P \<longleftrightarrow> P'"
+ and p2: "|- P' \<Longrightarrow> |- Q \<longleftrightarrow> Q'"
+ shows "|- (P \<and> Q) \<longleftrightarrow> (P' \<and> Q')"
apply (lem p1)
apply safe
apply (tactic \<open>
@@ -197,7 +197,7 @@
Cla.safe_tac @{context} 1)\<close>)
done
-lemma eq_sym_conv: "|- (x=y) <-> (y=x)"
+lemma eq_sym_conv: "|- x = y \<longleftrightarrow> y = x"
by (fast add!: subst)
ML_file "simpdata.ML"
@@ -207,14 +207,14 @@
text \<open>To create substition rules\<close>
-lemma eq_imp_subst: "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
+lemma eq_imp_subst: "|- a = b \<Longrightarrow> $H, A(a), $G |- $E, A(b), $F"
by simp
-lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
+lemma split_if: "|- P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) \<and> (\<not> Q \<longrightarrow> P(y)))"
apply (rule_tac P = Q in cut)
prefer 2
apply (simp add: if_P)
- apply (rule_tac P = "~Q" in cut)
+ apply (rule_tac P = "\<not> Q" in cut)
prefer 2
apply (simp add: if_not_P)
apply fast
@@ -225,7 +225,7 @@
apply fast
done
-lemma if_eq_cancel: "|- (if x=y then y else x) = x"
+lemma if_eq_cancel: "|- (if x = y then y else x) = x"
apply (lem split_if)
apply safe
apply (rule symL)
--- a/src/Sequents/LK/Hard_Quantifiers.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/LK/Hard_Quantifiers.thy Sat Oct 10 20:51:39 2015 +0200
@@ -15,251 +15,251 @@
imports "../LK"
begin
-lemma "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
+lemma "|- (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
by fast
-lemma "|- (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))"
+lemma "|- (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
by fast
-lemma "|- (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q"
+lemma "|- (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
by fast
-lemma "|- (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)"
+lemma "|- (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
by fast
text "Problems requiring quantifier duplication"
-(*Not provable by fast: needs multiple instantiation of ALL*)
-lemma "|- (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"
+(*Not provable by fast: needs multiple instantiation of \<forall>*)
+lemma "|- (\<forall>x. P(x) \<longrightarrow> P(f(x))) \<and> P(d) \<longrightarrow> P(f(f(f(d))))"
by best_dup
(*Needs double instantiation of the quantifier*)
-lemma "|- EX x. P(x) --> P(a) & P(b)"
+lemma "|- \<exists>x. P(x) \<longrightarrow> P(a) \<and> P(b)"
by fast_dup
-lemma "|- EX z. P(z) --> (ALL x. P(x))"
+lemma "|- \<exists>z. P(z) \<longrightarrow> (\<forall>x. P(x))"
by best_dup
text "Hard examples with quantifiers"
text "Problem 18"
-lemma "|- EX y. ALL x. P(y)-->P(x)"
+lemma "|- \<exists>y. \<forall>x. P(y)\<longrightarrow>P(x)"
by best_dup
text "Problem 19"
-lemma "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
+lemma "|- \<exists>x. \<forall>y z. (P(y)\<longrightarrow>Q(z)) \<longrightarrow> (P(x)\<longrightarrow>Q(x))"
by best_dup
text "Problem 20"
-lemma "|- (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))"
+lemma "|- (\<forall>x y. \<exists>z. \<forall>w. (P(x) \<and> Q(y)\<longrightarrow>R(z) \<and> S(w)))
+ \<longrightarrow> (\<exists>x y. P(x) \<and> Q(y)) \<longrightarrow> (\<exists>z. R(z))"
by fast
text "Problem 21"
-lemma "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"
+lemma "|- (\<exists>x. P \<longrightarrow> Q(x)) \<and> (\<exists>x. Q(x) \<longrightarrow> P) \<longrightarrow> (\<exists>x. P \<longleftrightarrow> Q(x))"
by best_dup
text "Problem 22"
-lemma "|- (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"
+lemma "|- (\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))"
by fast
text "Problem 23"
-lemma "|- (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))"
+lemma "|- (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x)))"
by best
text "Problem 24"
-lemma "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
- ~(EX x. P(x)) --> (EX x. Q(x)) & (ALL x. Q(x)|R(x) --> S(x))
- --> (EX x. P(x)&R(x))"
+lemma "|- \<not> (\<exists>x. S(x) \<and> Q(x)) \<and> (\<forall>x. P(x) \<longrightarrow> Q(x) \<or> R(x)) \<and>
+ \<not> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x)) \<and> (\<forall>x. Q(x) \<or> R(x) \<longrightarrow> S(x))
+ \<longrightarrow> (\<exists>x. P(x) \<and> R(x))"
by pc
text "Problem 25"
-lemma "|- (EX x. P(x)) &
- (ALL x. L(x) --> ~ (M(x) & R(x))) &
- (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))"
+lemma "|- (\<exists>x. P(x)) \<and>
+ (\<forall>x. L(x) \<longrightarrow> \<not> (M(x) \<and> R(x))) \<and>
+ (\<forall>x. P(x) \<longrightarrow> (M(x) \<and> L(x))) \<and>
+ ((\<forall>x. P(x)\<longrightarrow>Q(x)) \<or> (\<exists>x. P(x) \<and> R(x)))
+ \<longrightarrow> (\<exists>x. Q(x) \<and> P(x))"
by best
text "Problem 26"
-lemma "|- ((EX x. p(x)) <-> (EX x. q(x))) &
- (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))
- --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"
+lemma "|- ((\<exists>x. p(x)) \<longleftrightarrow> (\<exists>x. q(x))) \<and>
+ (\<forall>x. \<forall>y. p(x) \<and> q(y) \<longrightarrow> (r(x) \<longleftrightarrow> s(y)))
+ \<longrightarrow> ((\<forall>x. p(x)\<longrightarrow>r(x)) \<longleftrightarrow> (\<forall>x. q(x)\<longrightarrow>s(x)))"
by pc
text "Problem 27"
-lemma "|- (EX x. P(x) & ~Q(x)) &
- (ALL x. P(x) --> R(x)) &
- (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))"
+lemma "|- (\<exists>x. P(x) \<and> \<not> Q(x)) \<and>
+ (\<forall>x. P(x) \<longrightarrow> R(x)) \<and>
+ (\<forall>x. M(x) \<and> L(x) \<longrightarrow> P(x)) \<and>
+ ((\<exists>x. R(x) \<and> \<not> Q(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> \<not> R(x)))
+ \<longrightarrow> (\<forall>x. M(x) \<longrightarrow> \<not> L(x))"
by pc
text "Problem 28. AMENDED"
-lemma "|- (ALL x. P(x) --> (ALL x. Q(x))) &
- ((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))"
+lemma "|- (\<forall>x. P(x) \<longrightarrow> (\<forall>x. Q(x))) \<and>
+ ((\<forall>x. Q(x) \<or> R(x)) \<longrightarrow> (\<exists>x. Q(x) \<and> S(x))) \<and>
+ ((\<exists>x. S(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> M(x)))
+ \<longrightarrow> (\<forall>x. P(x) \<and> L(x) \<longrightarrow> M(x))"
by pc
text "Problem 29. Essentially the same as Principia Mathematica *11.71"
-lemma "|- (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)))"
+lemma "|- (\<exists>x. P(x)) \<and> (\<exists>y. Q(y))
+ \<longrightarrow> ((\<forall>x. P(x) \<longrightarrow> R(x)) \<and> (\<forall>y. Q(y) \<longrightarrow> S(y)) \<longleftrightarrow>
+ (\<forall>x y. P(x) \<and> Q(y) \<longrightarrow> R(x) \<and> S(y)))"
by pc
text "Problem 30"
-lemma "|- (ALL x. P(x) | Q(x) --> ~ R(x)) &
- (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
- --> (ALL x. S(x))"
+lemma "|- (\<forall>x. P(x) \<or> Q(x) \<longrightarrow> \<not> R(x)) \<and>
+ (\<forall>x. (Q(x) \<longrightarrow> \<not> S(x)) \<longrightarrow> P(x) \<and> R(x))
+ \<longrightarrow> (\<forall>x. S(x))"
by fast
text "Problem 31"
-lemma "|- ~(EX x. P(x) & (Q(x) | R(x))) &
- (EX x. L(x) & P(x)) &
- (ALL x. ~ R(x) --> M(x))
- --> (EX x. L(x) & M(x))"
+lemma "|- \<not> (\<exists>x. P(x) \<and> (Q(x) \<or> R(x))) \<and>
+ (\<exists>x. L(x) \<and> P(x)) \<and>
+ (\<forall>x. \<not> R(x) \<longrightarrow> M(x))
+ \<longrightarrow> (\<exists>x. L(x) \<and> M(x))"
by fast
text "Problem 32"
-lemma "|- (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
- (ALL x. S(x) & R(x) --> L(x)) &
- (ALL x. M(x) --> R(x))
- --> (ALL x. P(x) & M(x) --> L(x))"
+lemma "|- (\<forall>x. P(x) \<and> (Q(x) \<or> R(x)) \<longrightarrow> S(x)) \<and>
+ (\<forall>x. S(x) \<and> R(x) \<longrightarrow> L(x)) \<and>
+ (\<forall>x. M(x) \<longrightarrow> R(x))
+ \<longrightarrow> (\<forall>x. P(x) \<and> M(x) \<longrightarrow> L(x))"
by best
text "Problem 33"
-lemma "|- (ALL x. P(a) & (P(x)-->P(b))-->P(c)) <->
- (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
+lemma "|- (\<forall>x. P(a) \<and> (P(x) \<longrightarrow> P(b)) \<longrightarrow> P(c)) \<longleftrightarrow>
+ (\<forall>x. (\<not> P(a) \<or> P(x) \<or> P(c)) \<and> (\<not> P(a) \<or> \<not> P(b) \<or> P(c)))"
by fast
text "Problem 34 AMENDED (TWICE!!)"
(*Andrews's challenge*)
-lemma "|- ((EX x. ALL y. p(x) <-> p(y)) <->
- ((EX x. q(x)) <-> (ALL y. p(y)))) <->
- ((EX x. ALL y. q(x) <-> q(y)) <->
- ((EX x. p(x)) <-> (ALL y. q(y))))"
+lemma "|- ((\<exists>x. \<forall>y. p(x) \<longleftrightarrow> p(y)) \<longleftrightarrow>
+ ((\<exists>x. q(x)) \<longleftrightarrow> (\<forall>y. p(y)))) \<longleftrightarrow>
+ ((\<exists>x. \<forall>y. q(x) \<longleftrightarrow> q(y)) \<longleftrightarrow>
+ ((\<exists>x. p(x)) \<longleftrightarrow> (\<forall>y. q(y))))"
by best_dup
text "Problem 35"
-lemma "|- EX x y. P(x,y) --> (ALL u v. P(u,v))"
+lemma "|- \<exists>x y. P(x,y) \<longrightarrow> (\<forall>u v. P(u,v))"
by best_dup
text "Problem 36"
-lemma "|- (ALL x. EX y. J(x,y)) &
- (ALL x. EX y. G(x,y)) &
- (ALL x y. J(x,y) | G(x,y) -->
- (ALL z. J(y,z) | G(y,z) --> H(x,z)))
- --> (ALL x. EX y. H(x,y))"
+lemma "|- (\<forall>x. \<exists>y. J(x,y)) \<and>
+ (\<forall>x. \<exists>y. G(x,y)) \<and>
+ (\<forall>x y. J(x,y) \<or> G(x,y) \<longrightarrow>
+ (\<forall>z. J(y,z) \<or> G(y,z) \<longrightarrow> H(x,z)))
+ \<longrightarrow> (\<forall>x. \<exists>y. H(x,y))"
by fast
text "Problem 37"
-lemma "|- (ALL z. EX w. ALL x. EX y.
- (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) &
- (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &
- ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))
- --> (ALL x. EX y. R(x,y))"
+lemma "|- (\<forall>z. \<exists>w. \<forall>x. \<exists>y.
+ (P(x,z)\<longrightarrow>P(y,w)) \<and> P(y,z) \<and> (P(y,w) \<longrightarrow> (\<exists>u. Q(u,w)))) \<and>
+ (\<forall>x z. \<not> P(x,z) \<longrightarrow> (\<exists>y. Q(y,z))) \<and>
+ ((\<exists>x y. Q(x,y)) \<longrightarrow> (\<forall>x. R(x,x)))
+ \<longrightarrow> (\<forall>x. \<exists>y. R(x,y))"
by pc
text "Problem 38"
-lemma "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->
- (EX z. EX w. p(z) & r(x,w) & r(w,z))) <->
- (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &
- (~p(a) | ~(EX y. p(y) & r(x,y)) |
- (EX z. EX w. p(z) & r(x,w) & r(w,z))))"
+lemma "|- (\<forall>x. p(a) \<and> (p(x) \<longrightarrow> (\<exists>y. p(y) \<and> r(x,y))) \<longrightarrow>
+ (\<exists>z. \<exists>w. p(z) \<and> r(x,w) \<and> r(w,z))) \<longleftrightarrow>
+ (\<forall>x. (\<not> p(a) \<or> p(x) \<or> (\<exists>z. \<exists>w. p(z) \<and> r(x,w) \<and> r(w,z))) \<and>
+ (\<not> p(a) \<or> \<not> (\<exists>y. p(y) \<and> r(x,y)) \<or>
+ (\<exists>z. \<exists>w. p(z) \<and> r(x,w) \<and> r(w,z))))"
by pc
text "Problem 39"
-lemma "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
+lemma "|- \<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))"
by fast
text "Problem 40. AMENDED"
-lemma "|- (EX y. ALL x. F(x,y) <-> F(x,x)) -->
- ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
+lemma "|- (\<exists>y. \<forall>x. F(x,y) \<longleftrightarrow> F(x,x)) \<longrightarrow>
+ \<not> (\<forall>x. \<exists>y. \<forall>z. F(z,y) \<longleftrightarrow> \<not> F(z,x))"
by fast
text "Problem 41"
-lemma "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))
- --> ~ (EX z. ALL x. f(x,z))"
+lemma "|- (\<forall>z. \<exists>y. \<forall>x. f(x,y) \<longleftrightarrow> f(x,z) \<and> \<not> f(x,x))
+ \<longrightarrow> \<not> (\<exists>z. \<forall>x. f(x,z))"
by fast
text "Problem 42"
-lemma "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))"
+lemma "|- \<not> (\<exists>y. \<forall>x. p(x,y) \<longleftrightarrow> \<not> (\<exists>z. p(x,z) \<and> p(z,x)))"
oops
text "Problem 43"
-lemma "|- (ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y)))
- --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))"
+lemma "|- (\<forall>x. \<forall>y. q(x,y) \<longleftrightarrow> (\<forall>z. p(z,x) \<longleftrightarrow> p(z,y)))
+ \<longrightarrow> (\<forall>x. (\<forall>y. q(x,y) \<longleftrightarrow> q(y,x)))"
oops
text "Problem 44"
-lemma "|- (ALL x. f(x) -->
- (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) &
- (EX x. j(x) & (ALL y. g(y) --> h(x,y)))
- --> (EX x. j(x) & ~f(x))"
+lemma "|- (\<forall>x. f(x) \<longrightarrow>
+ (\<exists>y. g(y) \<and> h(x,y) \<and> (\<exists>y. g(y) \<and> \<not> h(x,y)))) \<and>
+ (\<exists>x. j(x) \<and> (\<forall>y. g(y) \<longrightarrow> h(x,y)))
+ \<longrightarrow> (\<exists>x. j(x) \<and> \<not> f(x))"
by fast
text "Problem 45"
-lemma "|- (ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))
- --> (ALL y. g(y) & h(x,y) --> k(y))) &
- ~ (EX y. l(y) & k(y)) &
- (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)))"
+lemma "|- (\<forall>x. f(x) \<and> (\<forall>y. g(y) \<and> h(x,y) \<longrightarrow> j(x,y))
+ \<longrightarrow> (\<forall>y. g(y) \<and> h(x,y) \<longrightarrow> k(y))) \<and>
+ \<not> (\<exists>y. l(y) \<and> k(y)) \<and>
+ (\<exists>x. f(x) \<and> (\<forall>y. h(x,y) \<longrightarrow> l(y))
+ \<and> (\<forall>y. g(y) \<and> h(x,y) \<longrightarrow> j(x,y)))
+ \<longrightarrow> (\<exists>x. f(x) \<and> \<not> (\<exists>y. g(y) \<and> h(x,y)))"
by best
text "Problems (mainly) involving equality or functions"
text "Problem 48"
-lemma "|- (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
+lemma "|- (a = b \<or> c = d) \<and> (a = c \<or> b = d) \<longrightarrow> a = d \<or> b = c"
by (fast add!: subst)
text "Problem 50"
-lemma "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
+lemma "|- (\<forall>x. P(a,x) \<or> (\<forall>y. P(x,y))) \<longrightarrow> (\<exists>x. \<forall>y. P(x,y))"
by best_dup
text "Problem 51"
-lemma "|- (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) -->
- (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
+lemma "|- (\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+ (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) \<longleftrightarrow> y = w) \<longleftrightarrow> x = z)"
by (fast add!: subst)
text "Problem 52" (*Almost the same as 51. *)
-lemma "|- (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) -->
- (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"
+lemma "|- (\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+ (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) \<longleftrightarrow> x = z) \<longleftrightarrow> y = w)"
by (fast add!: subst)
text "Problem 56"
-lemma "|- (ALL x.(EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
+lemma "|- (\<forall>x.(\<exists>y. P(y) \<and> x = f(y)) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> P(f(x)))"
by (best add: symL subst)
(*requires tricker to orient the equality properly*)
text "Problem 57"
-lemma "|- P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &
- (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"
+lemma "|- P(f(a,b), f(b,c)) \<and> P(f(b,c), f(a,c)) \<and>
+ (\<forall>x y z. P(x,y) \<and> P(y,z) \<longrightarrow> P(x,z)) \<longrightarrow> P(f(a,b), f(a,c))"
by fast
text "Problem 58!"
-lemma "|- (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
+lemma "|- (\<forall>x y. f(x) = g(y)) \<longrightarrow> (\<forall>x y. f(f(x)) = f(g(y)))"
by (fast add!: subst)
text "Problem 59"
(*Unification works poorly here -- the abstraction %sobj prevents efficient
operation of the occurs check*)
-lemma "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
+lemma "|- (\<forall>x. P(x) \<longleftrightarrow> \<not> P(f(x))) \<longrightarrow> (\<exists>x. P(x) \<and> \<not> P(f(x)))"
by best_dup
text "Problem 60"
-lemma "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
+lemma "|- \<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))"
by fast
text "Problem 62 as corrected in JAR 18 (1997), page 135"
-lemma "|- (ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x)))) <->
- (ALL x. (~p(a) | p(x) | p(f(f(x)))) &
- (~p(a) | ~p(f(x)) | p(f(f(x)))))"
+lemma "|- (\<forall>x. p(a) \<and> (p(x) \<longrightarrow> p(f(x))) \<longrightarrow> p(f(f(x)))) \<longleftrightarrow>
+ (\<forall>x. (\<not> p(a) \<or> p(x) \<or> p(f(f(x)))) \<and>
+ (\<not> p(a) \<or> \<not> p(f(x)) \<or> p(f(f(x)))))"
by fast
(*18 June 92: loaded in 372 secs*)
--- a/src/Sequents/LK/Nat.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/LK/Nat.thy Sat Oct 10 20:51:39 2015 +0200
@@ -14,19 +14,19 @@
axiomatization
Zero :: nat ("0") and
- Suc :: "nat=>nat" and
- rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
+ Suc :: "nat \<Rightarrow> nat" and
+ rec :: "[nat, 'a, [nat,'a] \<Rightarrow> 'a] \<Rightarrow> 'a"
where
- induct: "[| $H |- $E, P(0), $F;
- !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F" and
+ induct: "\<lbrakk>$H |- $E, P(0), $F;
+ \<And>x. $H, P(x) |- $E, P(Suc(x)), $F\<rbrakk> \<Longrightarrow> $H |- $E, P(n), $F" and
- Suc_inject: "|- Suc(m)=Suc(n) --> m=n" and
- Suc_neq_0: "|- Suc(m) ~= 0" and
+ Suc_inject: "|- Suc(m) = Suc(n) \<longrightarrow> m = n" and
+ Suc_neq_0: "|- Suc(m) \<noteq> 0" and
rec_0: "|- rec(0,a,f) = a" and
rec_Suc: "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
-definition add :: "[nat, nat] => nat" (infixl "+" 60)
- where "m + n == rec(m, n, %x y. Suc(y))"
+definition add :: "[nat, nat] \<Rightarrow> nat" (infixl "+" 60)
+ where "m + n == rec(m, n, \<lambda>x y. Suc(y))"
declare Suc_neq_0 [simp]
@@ -34,40 +34,40 @@
lemma Suc_inject_rule: "$H, $G, m = n |- $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G |- $E"
by (rule L_of_imp [OF Suc_inject])
-lemma Suc_n_not_n: "|- Suc(k) ~= k"
+lemma Suc_n_not_n: "|- Suc(k) \<noteq> k"
apply (rule_tac n = k in induct)
apply simp
apply (fast add!: Suc_inject_rule)
done
-lemma add_0: "|- 0+n = n"
+lemma add_0: "|- 0 + n = n"
apply (unfold add_def)
apply (rule rec_0)
done
-lemma add_Suc: "|- Suc(m)+n = Suc(m+n)"
+lemma add_Suc: "|- Suc(m) + n = Suc(m + n)"
apply (unfold add_def)
apply (rule rec_Suc)
done
declare add_0 [simp] add_Suc [simp]
-lemma add_assoc: "|- (k+m)+n = k+(m+n)"
+lemma add_assoc: "|- (k + m) + n = k + (m + n)"
apply (rule_tac n = "k" in induct)
apply simp_all
done
-lemma add_0_right: "|- m+0 = m"
+lemma add_0_right: "|- m + 0 = m"
apply (rule_tac n = "m" in induct)
apply simp_all
done
-lemma add_Suc_right: "|- m+Suc(n) = Suc(m+n)"
+lemma add_Suc_right: "|- m + Suc(n) = Suc(m + n)"
apply (rule_tac n = "m" in induct)
apply simp_all
done
-lemma "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)"
+lemma "(\<And>n. |- f(Suc(n)) = Suc(f(n))) \<Longrightarrow> |- f(i + j) = i + f(j)"
apply (rule_tac n = "i" in induct)
apply simp_all
done
--- a/src/Sequents/LK/Propositional.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/LK/Propositional.thy Sat Oct 10 20:51:39 2015 +0200
@@ -9,75 +9,75 @@
imports "../LK"
begin
-text "absorptive laws of & and | "
+text "absorptive laws of \<and> and \<or>"
-lemma "|- P & P <-> P"
+lemma "|- P \<and> P \<longleftrightarrow> P"
by fast_prop
-lemma "|- P | P <-> P"
+lemma "|- P \<or> P \<longleftrightarrow> P"
by fast_prop
-text "commutative laws of & and | "
+text "commutative laws of \<and> and \<or>"
-lemma "|- P & Q <-> Q & P"
+lemma "|- P \<and> Q \<longleftrightarrow> Q \<and> P"
by fast_prop
-lemma "|- P | Q <-> Q | P"
+lemma "|- P \<or> Q \<longleftrightarrow> Q \<or> P"
by fast_prop
-text "associative laws of & and | "
+text "associative laws of \<and> and \<or>"
-lemma "|- (P & Q) & R <-> P & (Q & R)"
+lemma "|- (P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
by fast_prop
-lemma "|- (P | Q) | R <-> P | (Q | R)"
+lemma "|- (P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
by fast_prop
-text "distributive laws of & and | "
+text "distributive laws of \<and> and \<or>"
-lemma "|- (P & Q) | R <-> (P | R) & (Q | R)"
+lemma "|- (P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)"
by fast_prop
-lemma "|- (P | Q) & R <-> (P & R) | (Q & R)"
+lemma "|- (P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R) \<or> (Q \<and> R)"
by fast_prop
text "Laws involving implication"
-lemma "|- (P|Q --> R) <-> (P-->R) & (Q-->R)"
+lemma "|- (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
by fast_prop
-lemma "|- (P & Q --> R) <-> (P--> (Q-->R))"
+lemma "|- (P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
by fast_prop
-lemma "|- (P --> Q & R) <-> (P-->Q) & (P-->R)"
+lemma "|- (P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
by fast_prop
text "Classical theorems"
-lemma "|- P|Q --> P| ~P&Q"
+lemma "|- P \<or> Q \<longrightarrow> P \<or> \<not> P \<and> Q"
by fast_prop
-lemma "|- (P-->Q)&(~P-->R) --> (P&Q | R)"
+lemma "|- (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<or> R)"
by fast_prop
-lemma "|- P&Q | ~P&R <-> (P-->Q)&(~P-->R)"
+lemma "|- P \<and> Q \<or> \<not> P \<and> R \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R)"
by fast_prop
-lemma "|- (P-->Q) | (P-->R) <-> (P --> Q | R)"
+lemma "|- (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
by fast_prop
(*If and only if*)
-lemma "|- (P<->Q) <-> (Q<->P)"
+lemma "|- (P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
by fast_prop
-lemma "|- ~ (P <-> ~P)"
+lemma "|- \<not> (P \<longleftrightarrow> \<not> P)"
by fast_prop
@@ -89,71 +89,71 @@
*)
(*1*)
-lemma "|- (P-->Q) <-> (~Q --> ~P)"
+lemma "|- (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
by fast_prop
(*2*)
-lemma "|- ~ ~ P <-> P"
+lemma "|- \<not> \<not> P \<longleftrightarrow> P"
by fast_prop
(*3*)
-lemma "|- ~(P-->Q) --> (Q-->P)"
+lemma "|- \<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
by fast_prop
(*4*)
-lemma "|- (~P-->Q) <-> (~Q --> P)"
+lemma "|- (\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"
by fast_prop
(*5*)
-lemma "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))"
+lemma "|- ((P \<or> Q) \<longrightarrow> (P \<or> R)) \<longrightarrow> (P \<or> (Q \<longrightarrow> R))"
by fast_prop
(*6*)
-lemma "|- P | ~ P"
+lemma "|- P \<or> \<not> P"
by fast_prop
(*7*)
-lemma "|- P | ~ ~ ~ P"
+lemma "|- P \<or> \<not> \<not> \<not> P"
by fast_prop
(*8. Peirce's law*)
-lemma "|- ((P-->Q) --> P) --> P"
+lemma "|- ((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
by fast_prop
(*9*)
-lemma "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
+lemma "|- ((P \<or> Q) \<and> (\<not> P \<or> Q) \<and> (P \<or> \<not> Q)) \<longrightarrow> \<not> (\<not> P \<or> \<not> Q)"
by fast_prop
(*10*)
-lemma "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q"
+lemma "Q \<longrightarrow> R, R \<longrightarrow> P \<and> Q, P \<longrightarrow> (Q \<or> R) |- P \<longleftrightarrow> Q"
by fast_prop
(*11. Proved in each direction (incorrectly, says Pelletier!!) *)
-lemma "|- P<->P"
+lemma "|- P \<longleftrightarrow> P"
by fast_prop
(*12. "Dijkstra's law"*)
-lemma "|- ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))"
+lemma "|- ((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
by fast_prop
(*13. Distributive law*)
-lemma "|- P | (Q & R) <-> (P | Q) & (P | R)"
+lemma "|- P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
by fast_prop
(*14*)
-lemma "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
+lemma "|- (P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P))"
by fast_prop
(*15*)
-lemma "|- (P --> Q) <-> (~P | Q)"
+lemma "|- (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
by fast_prop
(*16*)
-lemma "|- (P-->Q) | (Q-->P)"
+lemma "|- (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"
by fast_prop
(*17*)
-lemma "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
+lemma "|- ((P \<and> (Q \<longrightarrow> R)) \<longrightarrow> S) \<longleftrightarrow> ((\<not> P \<or> Q \<or> S) \<and> (\<not> P \<or> \<not> R \<or> S))"
by fast_prop
end
--- a/src/Sequents/LK/Quantifiers.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/LK/Quantifiers.thy Sat Oct 10 20:51:39 2015 +0200
@@ -9,94 +9,94 @@
imports "../LK"
begin
-lemma "|- (ALL x. P) <-> P"
+lemma "|- (\<forall>x. P) \<longleftrightarrow> P"
by fast
-lemma "|- (ALL x y. P(x,y)) <-> (ALL y x. P(x,y))"
+lemma "|- (\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
by fast
-lemma "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)"
+lemma "\<forall>u. P(u), \<forall>v. Q(v) |- \<forall>u v. P(u) \<and> Q(v)"
by fast
text "Permutation of existential quantifier."
-lemma "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))"
+lemma "|- (\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
by fast
-lemma "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
+lemma "|- (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
by fast
(*Converse is invalid*)
-lemma "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))"
+lemma "|- (\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
by fast
-text "Pushing ALL into an implication."
+text "Pushing \<forall>into an implication."
-lemma "|- (ALL x. P --> Q(x)) <-> (P --> (ALL x. Q(x)))"
+lemma "|- (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
by fast
-lemma "|- (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"
+lemma "|- (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
by fast
-lemma "|- (EX x. P) <-> P"
+lemma "|- (\<exists>x. P) \<longleftrightarrow> P"
by fast
-text "Distribution of EX over disjunction."
+text "Distribution of \<exists>over disjunction."
-lemma "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
+lemma "|- (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
by fast
(*Converse is invalid*)
-lemma "|- (EX x. P(x) & Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"
+lemma "|- (\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
by fast
text "Harder examples: classical theorems."
-lemma "|- (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))"
+lemma "|- (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
by fast
-lemma "|- (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q"
+lemma "|- (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
by fast
-lemma "|- (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)"
+lemma "|- (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
by fast
text "Basic test of quantifier reasoning"
-lemma "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
+lemma "|- (\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
by fast
-lemma "|- (ALL x. Q(x)) --> (EX x. Q(x))"
+lemma "|- (\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
by fast
text "The following are invalid!"
(*INVALID*)
-lemma "|- (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"
+lemma "|- (\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
apply fast?
apply (rule _)
oops
(*INVALID*)
-lemma "|- (EX x. Q(x)) --> (ALL x. Q(x))"
+lemma "|- (\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
apply fast?
apply (rule _)
oops
(*INVALID*)
-schematic_goal "|- P(?a) --> (ALL x. P(x))"
+schematic_goal "|- P(?a) \<longrightarrow> (\<forall>x. P(x))"
apply fast?
apply (rule _)
oops
(*INVALID*)
-schematic_goal "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
+schematic_goal "|- (P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))"
apply fast?
apply (rule _)
oops
@@ -104,35 +104,35 @@
text "Back to things that are provable..."
-lemma "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
+lemma "|- (\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
by fast
(*An example of why exR should be delayed as long as possible*)
-lemma "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))"
+lemma "|- (P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
by fast
text "Solving for a Var"
-schematic_goal "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
+schematic_goal "|- (\<forall>x. P(x) \<longrightarrow> Q(f(x))) \<and> (\<forall>x. Q(x) \<longrightarrow> R(g(x))) \<and> P(d) \<longrightarrow> R(?a)"
by fast
text "Principia Mathematica *11.53"
-lemma "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
+lemma "|- (\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))"
by fast
text "Principia Mathematica *11.55"
-lemma "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
+lemma "|- (\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))"
by fast
text "Principia Mathematica *11.61"
-lemma "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
+lemma "|- (\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))"
by fast
--- a/src/Sequents/LK0.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/LK0.thy Sat Oct 10 20:51:39 2015 +0200
@@ -21,15 +21,15 @@
True :: o
False :: o
- equal :: "['a,'a] => o" (infixl "=" 50)
- Not :: "o => o" ("~ _" [40] 40)
- conj :: "[o,o] => o" (infixr "&" 35)
- disj :: "[o,o] => o" (infixr "|" 30)
- imp :: "[o,o] => o" (infixr "-->" 25)
- iff :: "[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)
+ equal :: "['a,'a] \<Rightarrow> o" (infixl "=" 50)
+ Not :: "o \<Rightarrow> o" ("\<not> _" [40] 40)
+ conj :: "[o,o] \<Rightarrow> o" (infixr "\<and>" 35)
+ disj :: "[o,o] \<Rightarrow> o" (infixr "\<or>" 30)
+ imp :: "[o,o] \<Rightarrow> o" (infixr "\<longrightarrow>" 25)
+ iff :: "[o,o] \<Rightarrow> o" (infixr "\<longleftrightarrow>" 25)
+ The :: "('a \<Rightarrow> o) \<Rightarrow> 'a" (binder "THE " 10)
+ All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10)
+ Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)
syntax
"_Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
@@ -38,108 +38,98 @@
print_translation \<open>[(@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))]\<close>
abbreviation
- not_equal (infixl "~=" 50) where
- "x ~= y == ~ (x = y)"
-
-notation (xsymbols)
- Not ("\<not> _" [40] 40) and
- conj (infixr "\<and>" 35) and
- disj (infixr "\<or>" 30) and
- imp (infixr "\<longrightarrow>" 25) and
- iff (infixr "\<longleftrightarrow>" 25) and
- All (binder "\<forall>" 10) and
- Ex (binder "\<exists>" 10) and
- not_equal (infixl "\<noteq>" 50)
+ not_equal (infixl "\<noteq>" 50) where
+ "x \<noteq> y \<equiv> \<not> (x = y)"
axiomatization where
(*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
- contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F" and
- contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E" and
+ contRS: "$H |- $E, $S, $S, $F \<Longrightarrow> $H |- $E, $S, $F" and
+ contLS: "$H, $S, $S, $G |- $E \<Longrightarrow> $H, $S, $G |- $E" and
- thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F" and
- thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E" and
+ thinRS: "$H |- $E, $F \<Longrightarrow> $H |- $E, $S, $F" and
+ thinLS: "$H, $G |- $E \<Longrightarrow> $H, $S, $G |- $E" and
- exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F" and
- exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E" and
+ exchRS: "$H |- $E, $R, $S, $F \<Longrightarrow> $H |- $E, $S, $R, $F" and
+ exchLS: "$H, $R, $S, $G |- $E \<Longrightarrow> $H, $S, $R, $G |- $E" and
- cut: "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E" and
+ cut: "\<lbrakk>$H |- $E, P; $H, P |- $E\<rbrakk> \<Longrightarrow> $H |- $E" and
(*Propositional rules*)
basic: "$H, P, $G |- $E, P, $F" and
- 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
+ conjR: "\<lbrakk>$H|- $E, P, $F; $H|- $E, Q, $F\<rbrakk> \<Longrightarrow> $H|- $E, P \<and> Q, $F" and
+ conjL: "$H, P, Q, $G |- $E \<Longrightarrow> $H, P \<and> Q, $G |- $E" and
- 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
+ disjR: "$H |- $E, P, Q, $F \<Longrightarrow> $H |- $E, P \<or> Q, $F" and
+ disjL: "\<lbrakk>$H, P, $G |- $E; $H, Q, $G |- $E\<rbrakk> \<Longrightarrow> $H, P \<or> Q, $G |- $E" and
- 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
+ impR: "$H, P |- $E, Q, $F \<Longrightarrow> $H |- $E, P \<longrightarrow> Q, $F" and
+ impL: "\<lbrakk>$H,$G |- $E,P; $H, Q, $G |- $E\<rbrakk> \<Longrightarrow> $H, P \<longrightarrow> Q, $G |- $E" and
- notR: "$H, P |- $E, $F ==> $H |- $E, ~P, $F" and
- notL: "$H, $G |- $E, P ==> $H, ~P, $G |- $E" and
+ notR: "$H, P |- $E, $F \<Longrightarrow> $H |- $E, \<not> P, $F" and
+ notL: "$H, $G |- $E, P \<Longrightarrow> $H, \<not> P, $G |- $E" and
FalseL: "$H, False, $G |- $E" and
- True_def: "True == False-->False" and
- iff_def: "P<->Q == (P-->Q) & (Q-->P)"
+ True_def: "True \<equiv> False \<longrightarrow> False" and
+ iff_def: "P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)"
axiomatization where
(*Quantifiers*)
- 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
+ allR: "(\<And>x. $H |- $E, P(x), $F) \<Longrightarrow> $H |- $E, \<forall>x. P(x), $F" and
+ allL: "$H, P(x), $G, \<forall>x. P(x) |- $E \<Longrightarrow> $H, \<forall>x. P(x), $G |- $E" and
- 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
+ exR: "$H |- $E, P(x), $F, \<exists>x. P(x) \<Longrightarrow> $H |- $E, \<exists>x. P(x), $F" and
+ exL: "(\<And>x. $H, P(x), $G |- $E) \<Longrightarrow> $H, \<exists>x. P(x), $G |- $E" and
(*Equality*)
- 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)"
+ refl: "$H |- $E, a = a, $F" and
+ subst: "\<And>G H E. $H(a), $G(a) |- $E(a) \<Longrightarrow> $H(b), a=b, $G(b) |- $E(b)"
(* Reflection *)
axiomatization where
- eq_reflection: "|- x=y ==> (x==y)" and
- iff_reflection: "|- P<->Q ==> (P==Q)"
+ eq_reflection: "|- x = y \<Longrightarrow> (x \<equiv> y)" and
+ iff_reflection: "|- P \<longleftrightarrow> Q \<Longrightarrow> (P \<equiv> 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"
+ The: "\<lbrakk>$H |- $E, P(a), $F; \<And>x.$H, P(x) |- $E, x=a, $F\<rbrakk> \<Longrightarrow>
+ $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] \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" 10)
+ where "If(P,x,y) \<equiv> THE z::'a. (P \<longrightarrow> z = x) \<and> (\<not> P \<longrightarrow> z = y)"
(** Structural Rules on formulas **)
(*contraction*)
-lemma contR: "$H |- $E, P, P, $F ==> $H |- $E, P, $F"
+lemma contR: "$H |- $E, P, P, $F \<Longrightarrow> $H |- $E, P, $F"
by (rule contRS)
-lemma contL: "$H, P, P, $G |- $E ==> $H, P, $G |- $E"
+lemma contL: "$H, P, P, $G |- $E \<Longrightarrow> $H, P, $G |- $E"
by (rule contLS)
(*thinning*)
-lemma thinR: "$H |- $E, $F ==> $H |- $E, P, $F"
+lemma thinR: "$H |- $E, $F \<Longrightarrow> $H |- $E, P, $F"
by (rule thinRS)
-lemma thinL: "$H, $G |- $E ==> $H, P, $G |- $E"
+lemma thinL: "$H, $G |- $E \<Longrightarrow> $H, P, $G |- $E"
by (rule thinLS)
(*exchange*)
-lemma exchR: "$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F"
+lemma exchR: "$H |- $E, Q, P, $F \<Longrightarrow> $H |- $E, P, Q, $F"
by (rule exchRS)
-lemma exchL: "$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E"
+lemma exchL: "$H, Q, P, $G |- $E \<Longrightarrow> $H, P, Q, $G |- $E"
by (rule exchLS)
ML \<open>
@@ -156,19 +146,17 @@
(** If-and-only-if rules **)
-lemma iffR:
- "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
+lemma iffR: "\<lbrakk>$H,P |- $E,Q,$F; $H,Q |- $E,P,$F\<rbrakk> \<Longrightarrow> $H |- $E, P \<longleftrightarrow> Q, $F"
apply (unfold iff_def)
apply (assumption | rule conjR impR)+
done
-lemma iffL:
- "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
+lemma iffL: "\<lbrakk>$H,$G |- $E,P,Q; $H,Q,P,$G |- $E\<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G |- $E"
apply (unfold iff_def)
apply (assumption | rule conjL impL basic)+
done
-lemma iff_refl: "$H |- $E, (P <-> P), $F"
+lemma iff_refl: "$H |- $E, (P \<longleftrightarrow> P), $F"
apply (rule iffR basic)+
done
@@ -181,7 +169,7 @@
(*Descriptions*)
lemma the_equality:
assumes p1: "$H |- $E, P(a), $F"
- and p2: "!!x. $H, P(x) |- $E, x=a, $F"
+ and p2: "\<And>x. $H, P(x) |- $E, x=a, $F"
shows "$H |- $E, (THE x. P(x)) = a, $F"
apply (rule cut)
apply (rule_tac [2] p2)
@@ -192,12 +180,12 @@
(** Weakened quantifier rules. Incomplete, they let the search terminate.**)
-lemma allL_thin: "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E"
+lemma allL_thin: "$H, P(x), $G |- $E \<Longrightarrow> $H, \<forall>x. P(x), $G |- $E"
apply (rule allL)
apply (erule thinL)
done
-lemma exR_thin: "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F"
+lemma exR_thin: "$H |- $E, P(x), $F \<Longrightarrow> $H |- $E, \<exists>x. P(x), $F"
apply (rule exR)
apply (erule thinR)
done
@@ -245,7 +233,7 @@
lemma mp_R:
- assumes major: "$H |- $E, $F, P --> Q"
+ assumes major: "$H |- $E, $F, P \<longrightarrow> Q"
and minor: "$H |- $E, $F, P"
shows "$H |- $E, Q, $F"
apply (rule thinRS [THEN cut], rule major)
@@ -254,7 +242,7 @@
done
lemma mp_L:
- assumes major: "$H, $G |- $E, P --> Q"
+ assumes major: "$H, $G |- $E, P \<longrightarrow> Q"
and minor: "$H, $G, Q |- $E"
shows "$H, P, $G |- $E"
apply (rule thinL [THEN cut], rule major)
@@ -266,7 +254,7 @@
(** Two rules to generate left- and right- rules from implications **)
lemma R_of_imp:
- assumes major: "|- P --> Q"
+ assumes major: "|- P \<longrightarrow> Q"
and minor: "$H |- $E, $F, P"
shows "$H |- $E, Q, $F"
apply (rule mp_R)
@@ -275,7 +263,7 @@
done
lemma L_of_imp:
- assumes major: "|- P --> Q"
+ assumes major: "|- P \<longrightarrow> Q"
and minor: "$H, $G, Q |- $E"
shows "$H, P, $G |- $E"
apply (rule mp_L)
@@ -285,24 +273,24 @@
(*Can be used to create implications in a subgoal*)
lemma backwards_impR:
- assumes prem: "$H, $G |- $E, $F, P --> Q"
+ assumes prem: "$H, $G |- $E, $F, P \<longrightarrow> Q"
shows "$H, P, $G |- $E, Q, $F"
apply (rule mp_L)
apply (rule_tac [2] basic)
apply (rule thinR, rule prem)
done
-lemma conjunct1: "|-P&Q ==> |-P"
+lemma conjunct1: "|-P \<and> Q \<Longrightarrow> |-P"
apply (erule thinR [THEN cut])
apply fast
done
-lemma conjunct2: "|-P&Q ==> |-Q"
+lemma conjunct2: "|-P \<and> Q \<Longrightarrow> |-Q"
apply (erule thinR [THEN cut])
apply fast
done
-lemma spec: "|- (ALL x. P(x)) ==> |- P(x)"
+lemma spec: "|- (\<forall>x. P(x)) \<Longrightarrow> |- P(x)"
apply (erule thinR [THEN cut])
apply fast
done
@@ -310,10 +298,10 @@
(** Equality **)
-lemma sym: "|- a=b --> b=a"
+lemma sym: "|- a = b \<longrightarrow> b = a"
by (safe add!: subst)
-lemma trans: "|- a=b --> b=c --> a=c"
+lemma trans: "|- a = b \<longrightarrow> b = c \<longrightarrow> a = c"
by (safe add!: subst)
(* Symmetry of equality in hypotheses *)
@@ -322,18 +310,18 @@
(* Symmetry of equality in hypotheses *)
lemmas symR = sym [THEN R_of_imp]
-lemma transR: "[| $H|- $E, $F, a=b; $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F"
+lemma transR: "\<lbrakk>$H|- $E, $F, a = b; $H|- $E, $F, b=c\<rbrakk> \<Longrightarrow> $H|- $E, a = c, $F"
by (rule trans [THEN R_of_imp, THEN mp_R])
(* Two theorms for rewriting only one instance of a definition:
the first for definitions of formulae and the second for terms *)
-lemma def_imp_iff: "(A == B) ==> |- A <-> B"
+lemma def_imp_iff: "(A \<equiv> B) \<Longrightarrow> |- A \<longleftrightarrow> B"
apply unfold
apply (rule iff_refl)
done
-lemma meta_eq_to_obj_eq: "(A == B) ==> |- A = B"
+lemma meta_eq_to_obj_eq: "(A \<equiv> B) \<Longrightarrow> |- A = B"
apply unfold
apply (rule refl)
done
@@ -347,13 +335,13 @@
lemma if_False: "|- (if False then x else y) = y"
unfolding If_def by fast
-lemma if_P: "|- P ==> |- (if P then x else y) = x"
+lemma if_P: "|- P \<Longrightarrow> |- (if P then x else y) = x"
apply (unfold If_def)
apply (erule thinR [THEN cut])
apply fast
done
-lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y"
+lemma if_not_P: "|- \<not> P \<Longrightarrow> |- (if P then x else y) = y"
apply (unfold If_def)
apply (erule thinR [THEN cut])
apply fast
--- a/src/Sequents/Modal0.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/Modal0.thy Sat Oct 10 20:51:39 2015 +0200
@@ -10,10 +10,10 @@
ML_file "modal.ML"
consts
- box :: "o=>o" ("[]_" [50] 50)
- dia :: "o=>o" ("<>_" [50] 50)
- strimp :: "[o,o]=>o" (infixr "--<" 25)
- streqv :: "[o,o]=>o" (infixr ">-<" 25)
+ box :: "o\<Rightarrow>o" ("[]_" [50] 50)
+ dia :: "o\<Rightarrow>o" ("<>_" [50] 50)
+ strimp :: "[o,o]\<Rightarrow>o" (infixr "--<" 25)
+ streqv :: "[o,o]\<Rightarrow>o" (infixr ">-<" 25)
Lstar :: "two_seqi"
Rstar :: "two_seqi"
@@ -37,20 +37,18 @@
\<close>
defs
- strimp_def: "P --< Q == [](P --> Q)"
- streqv_def: "P >-< Q == (P --< Q) & (Q --< P)"
+ strimp_def: "P --< Q == [](P \<longrightarrow> Q)"
+ streqv_def: "P >-< Q == (P --< Q) \<and> (Q --< P)"
lemmas rewrite_rls = strimp_def streqv_def
-lemma iffR:
- "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
+lemma iffR: "\<lbrakk>$H,P |- $E,Q,$F; $H,Q |- $E,P,$F\<rbrakk> \<Longrightarrow> $H |- $E, P \<longleftrightarrow> Q, $F"
apply (unfold iff_def)
apply (assumption | rule conjR impR)+
done
-lemma iffL:
- "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
+lemma iffL: "\<lbrakk>$H,$G |- $E,P,Q; $H,Q,P,$G |- $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G |- $E"
apply (unfold iff_def)
apply (assumption | rule conjL impL basic)+
done
--- a/src/Sequents/S4.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/S4.thy Sat Oct 10 20:51:39 2015 +0200
@@ -13,23 +13,23 @@
(* delta * == {<>P | <>P : delta} *)
lstar0: "|L>" and
- lstar1: "$G |L> $H ==> []P, $G |L> []P, $H" and
- lstar2: "$G |L> $H ==> P, $G |L> $H" and
+ lstar1: "$G |L> $H \<Longrightarrow> []P, $G |L> []P, $H" and
+ lstar2: "$G |L> $H \<Longrightarrow> 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
+ rstar1: "$G |R> $H \<Longrightarrow> <>P, $G |R> <>P, $H" and
+ rstar2: "$G |R> $H \<Longrightarrow> 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" and
- boxL: "$E,P,$F,[]P |- $G ==> $E, []P, $F |- $G" and
+ "\<lbrakk>$E |L> $E'; $F |R> $F'; $G |R> $G';
+ $E' |- $F', P, $G'\<rbrakk> \<Longrightarrow> $E |- $F, []P, $G" and
+ boxL: "$E,P,$F,[]P |- $G \<Longrightarrow> $E, []P, $F |- $G" and
- diaR: "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G" and
+ diaR: "$E |- $F,P,$G,<>P \<Longrightarrow> $E |- $F, <>P, $G" and
diaL:
- "[| $E |L> $E'; $F |L> $F'; $G |R> $G';
- $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G"
+ "\<lbrakk>$E |L> $E'; $F |L> $F'; $G |R> $G';
+ $E', P, $F' |- $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F |- $G"
ML \<open>
structure S4_Prover = Modal_ProverFun
@@ -49,63 +49,63 @@
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
-lemma "|- []P --> P" by S4_solve
-lemma "|- [](P-->Q) --> ([]P-->[]Q)" by S4_solve (* normality*)
-lemma "|- (P--<Q) --> []P --> []Q" by S4_solve
-lemma "|- P --> <>P" by S4_solve
+lemma "|- []P \<longrightarrow> P" by S4_solve
+lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by S4_solve (* normality*)
+lemma "|- (P --< Q) \<longrightarrow> []P \<longrightarrow> []Q" by S4_solve
+lemma "|- P \<longrightarrow> <>P" by S4_solve
-lemma "|- [](P & Q) <-> []P & []Q" by S4_solve
-lemma "|- <>(P | Q) <-> <>P | <>Q" by S4_solve
-lemma "|- [](P<->Q) <-> (P>-<Q)" by S4_solve
-lemma "|- <>(P-->Q) <-> ([]P--><>Q)" by S4_solve
-lemma "|- []P <-> ~<>(~P)" by S4_solve
-lemma "|- [](~P) <-> ~<>P" by S4_solve
-lemma "|- ~[]P <-> <>(~P)" by S4_solve
-lemma "|- [][]P <-> ~<><>(~P)" by S4_solve
-lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by S4_solve
+lemma "|- [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S4_solve
+lemma "|- <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S4_solve
+lemma "|- [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P >-< Q)" by S4_solve
+lemma "|- <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S4_solve
+lemma "|- []P \<longleftrightarrow> \<not> <>(\<not> P)" by S4_solve
+lemma "|- [](\<not> P) \<longleftrightarrow> \<not> <>P" by S4_solve
+lemma "|- \<not> []P \<longleftrightarrow> <>(\<not> P)" by S4_solve
+lemma "|- [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by S4_solve
+lemma "|- \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>Q" by S4_solve
-lemma "|- []P | []Q --> [](P | Q)" by S4_solve
-lemma "|- <>(P & Q) --> <>P & <>Q" by S4_solve
-lemma "|- [](P | Q) --> []P | <>Q" by S4_solve
-lemma "|- <>P & []Q --> <>(P & Q)" by S4_solve
-lemma "|- [](P | Q) --> <>P | []Q" by S4_solve
-lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by S4_solve
-lemma "|- (P--<Q) & (Q--<R) --> (P--<R)" by S4_solve
-lemma "|- []P --> <>Q --> <>(P & Q)" by S4_solve
+lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S4_solve
+lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S4_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S4_solve
+lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S4_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S4_solve
+lemma "|- <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by S4_solve
+lemma "|- (P --< Q) \<and> (Q --< R) \<longrightarrow> (P --< R)" by S4_solve
+lemma "|- []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by S4_solve
(* Theorems of system S4 from Hughes and Cresswell, p.46 *)
-lemma "|- []A --> A" by S4_solve (* refexivity *)
-lemma "|- []A --> [][]A" by S4_solve (* transitivity *)
-lemma "|- []A --> <>A" by S4_solve (* seriality *)
-lemma "|- <>[](<>A --> []<>A)" by S4_solve
-lemma "|- <>[](<>[]A --> []A)" by S4_solve
-lemma "|- []P <-> [][]P" by S4_solve
-lemma "|- <>P <-> <><>P" by S4_solve
-lemma "|- <>[]<>P --> <>P" by S4_solve
-lemma "|- []<>P <-> []<>[]<>P" by S4_solve
-lemma "|- <>[]P <-> <>[]<>[]P" by S4_solve
+lemma "|- []A \<longrightarrow> A" by S4_solve (* refexivity *)
+lemma "|- []A \<longrightarrow> [][]A" by S4_solve (* transitivity *)
+lemma "|- []A \<longrightarrow> <>A" by S4_solve (* seriality *)
+lemma "|- <>[](<>A \<longrightarrow> []<>A)" by S4_solve
+lemma "|- <>[](<>[]A \<longrightarrow> []A)" by S4_solve
+lemma "|- []P \<longleftrightarrow> [][]P" by S4_solve
+lemma "|- <>P \<longleftrightarrow> <><>P" by S4_solve
+lemma "|- <>[]<>P \<longrightarrow> <>P" by S4_solve
+lemma "|- []<>P \<longleftrightarrow> []<>[]<>P" by S4_solve
+lemma "|- <>[]P \<longleftrightarrow> <>[]<>[]P" by S4_solve
(* Theorems for system S4 from Hughes and Cresswell, p.60 *)
-lemma "|- []P | []Q <-> []([]P | []Q)" by S4_solve
-lemma "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)" by S4_solve
+lemma "|- []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S4_solve
+lemma "|- ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S4_solve
(* These are from Hailpern, LNCS 129 *)
-lemma "|- [](P & Q) <-> []P & []Q" by S4_solve
-lemma "|- <>(P | Q) <-> <>P | <>Q" by S4_solve
-lemma "|- <>(P --> Q) <-> ([]P --> <>Q)" by S4_solve
+lemma "|- [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S4_solve
+lemma "|- <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S4_solve
+lemma "|- <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S4_solve
-lemma "|- [](P --> Q) --> (<>P --> <>Q)" by S4_solve
-lemma "|- []P --> []<>P" by S4_solve
-lemma "|- <>[]P --> <>P" by S4_solve
+lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> (<>P \<longrightarrow> <>Q)" by S4_solve
+lemma "|- []P \<longrightarrow> []<>P" by S4_solve
+lemma "|- <>[]P \<longrightarrow> <>P" by S4_solve
-lemma "|- []P | []Q --> [](P | Q)" by S4_solve
-lemma "|- <>(P & Q) --> <>P & <>Q" by S4_solve
-lemma "|- [](P | Q) --> []P | <>Q" by S4_solve
-lemma "|- <>P & []Q --> <>(P & Q)" by S4_solve
-lemma "|- [](P | Q) --> <>P | []Q" by S4_solve
+lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S4_solve
+lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S4_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S4_solve
+lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S4_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S4_solve
end
--- a/src/Sequents/S43.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/S43.thy Sat Oct 10 20:51:39 2015 +0200
@@ -10,10 +10,10 @@
begin
consts
- S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
- seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+ S43pi :: "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq',
+ seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
syntax
- "_S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
+ "_S43pi" :: "[seq, seq, seq, seq, seq, seq] \<Rightarrow> prop"
("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
parse_translation \<open>
@@ -38,11 +38,11 @@
(* delta * == {<>P | <>P : delta} *)
lstar0: "|L>" and
- lstar1: "$G |L> $H ==> []P, $G |L> []P, $H" and
- lstar2: "$G |L> $H ==> P, $G |L> $H" and
+ lstar1: "$G |L> $H \<Longrightarrow> []P, $G |L> []P, $H" and
+ lstar2: "$G |L> $H \<Longrightarrow> 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
+ rstar1: "$G |R> $H \<Longrightarrow> <>P, $G |R> <>P, $H" and
+ rstar2: "$G |R> $H \<Longrightarrow> P, $G |R> $H" and
(* Set of Horn clauses to generate the antecedents for the S43 pi rule *)
(* ie *)
@@ -56,23 +56,23 @@
S43pi0: "S43pi $L;; $R;; $Lbox; $Rdia" and
S43pi1:
- "[| (S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox |- $R,$Rdia |] ==>
+ "\<lbrakk>(S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox |- $R,$Rdia\<rbrakk> \<Longrightarrow>
S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia" and
S43pi2:
- "[| (S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox |- $R',P,$R,$Rdia |] ==>
+ "\<lbrakk>(S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox |- $R',P,$R,$Rdia\<rbrakk> \<Longrightarrow>
S43pi $L';; $R'; []P,$R; $Lbox;$Rdia" and
(* Rules for [] and <> for S43 *)
- boxL: "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G" and
- diaR: "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G" and
+ boxL: "$E, P, $F, []P |- $G \<Longrightarrow> $E, []P, $F |- $G" and
+ diaR: "$E |- $F, P, $G, <>P \<Longrightarrow> $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 |] ==>
+ "\<lbrakk>$L1,<>P,$L2 |L> $Lbox; $L1,<>P,$L2 |R> $Ldia; $R |L> $Rbox; $R |R> $Rdia;
+ S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia\<rbrakk> \<Longrightarrow>
$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 |] ==>
+ "\<lbrakk>$L |L> $Lbox; $L |R> $Ldia; $R1,[]P,$R2 |L> $Rbox; $R1,[]P,$R2 |R> $Rdia;
+ S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia\<rbrakk> \<Longrightarrow>
$L |- $R1, []P, $R2"
@@ -97,108 +97,108 @@
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
-lemma "|- []P --> P" by S43_solve
-lemma "|- [](P-->Q) --> ([]P-->[]Q)" by S43_solve (* normality*)
-lemma "|- (P--<Q) --> []P --> []Q" by S43_solve
-lemma "|- P --> <>P" by S43_solve
+lemma "|- []P \<longrightarrow> P" by S43_solve
+lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by S43_solve (* normality*)
+lemma "|- (P--<Q) \<longrightarrow> []P \<longrightarrow> []Q" by S43_solve
+lemma "|- P \<longrightarrow> <>P" by S43_solve
-lemma "|- [](P & Q) <-> []P & []Q" by S43_solve
-lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve
-lemma "|- [](P<->Q) <-> (P>-<Q)" by S43_solve
-lemma "|- <>(P-->Q) <-> ([]P--><>Q)" by S43_solve
-lemma "|- []P <-> ~<>(~P)" by S43_solve
-lemma "|- [](~P) <-> ~<>P" by S43_solve
-lemma "|- ~[]P <-> <>(~P)" by S43_solve
-lemma "|- [][]P <-> ~<><>(~P)" by S43_solve
-lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by S43_solve
+lemma "|- [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
+lemma "|- <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
+lemma "|- [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P>-<Q)" by S43_solve
+lemma "|- <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S43_solve
+lemma "|- []P \<longleftrightarrow> \<not> <>(\<not> P)" by S43_solve
+lemma "|- [](\<not>P) \<longleftrightarrow> \<not> <>P" by S43_solve
+lemma "|- \<not> []P \<longleftrightarrow> <>(\<not> P)" by S43_solve
+lemma "|- [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by S43_solve
+lemma "|- \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>Q" by S43_solve
-lemma "|- []P | []Q --> [](P | Q)" by S43_solve
-lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve
-lemma "|- [](P | Q) --> []P | <>Q" by S43_solve
-lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve
-lemma "|- [](P | Q) --> <>P | []Q" by S43_solve
-lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by S43_solve
-lemma "|- (P--<Q) & (Q--<R) --> (P--<R)" by S43_solve
-lemma "|- []P --> <>Q --> <>(P & Q)" by S43_solve
+lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
+lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
+lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
+lemma "|- <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by S43_solve
+lemma "|- (P --< Q) \<and> (Q --<R ) \<longrightarrow> (P --< R)" by S43_solve
+lemma "|- []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
(* Theorems of system S4 from Hughes and Cresswell, p.46 *)
-lemma "|- []A --> A" by S43_solve (* refexivity *)
-lemma "|- []A --> [][]A" by S43_solve (* transitivity *)
-lemma "|- []A --> <>A" by S43_solve (* seriality *)
-lemma "|- <>[](<>A --> []<>A)" by S43_solve
-lemma "|- <>[](<>[]A --> []A)" by S43_solve
-lemma "|- []P <-> [][]P" by S43_solve
-lemma "|- <>P <-> <><>P" by S43_solve
-lemma "|- <>[]<>P --> <>P" by S43_solve
-lemma "|- []<>P <-> []<>[]<>P" by S43_solve
-lemma "|- <>[]P <-> <>[]<>[]P" by S43_solve
+lemma "|- []A \<longrightarrow> A" by S43_solve (* refexivity *)
+lemma "|- []A \<longrightarrow> [][]A" by S43_solve (* transitivity *)
+lemma "|- []A \<longrightarrow> <>A" by S43_solve (* seriality *)
+lemma "|- <>[](<>A \<longrightarrow> []<>A)" by S43_solve
+lemma "|- <>[](<>[]A \<longrightarrow> []A)" by S43_solve
+lemma "|- []P \<longleftrightarrow> [][]P" by S43_solve
+lemma "|- <>P \<longleftrightarrow> <><>P" by S43_solve
+lemma "|- <>[]<>P \<longrightarrow> <>P" by S43_solve
+lemma "|- []<>P \<longleftrightarrow> []<>[]<>P" by S43_solve
+lemma "|- <>[]P \<longleftrightarrow> <>[]<>[]P" by S43_solve
(* Theorems for system S4 from Hughes and Cresswell, p.60 *)
-lemma "|- []P | []Q <-> []([]P | []Q)" by S43_solve
-lemma "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)" by S43_solve
+lemma "|- []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S43_solve
+lemma "|- ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S43_solve
(* These are from Hailpern, LNCS 129 *)
-lemma "|- [](P & Q) <-> []P & []Q" by S43_solve
-lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve
-lemma "|- <>(P --> Q) <-> ([]P --> <>Q)" by S43_solve
+lemma "|- [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
+lemma "|- <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
+lemma "|- <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S43_solve
-lemma "|- [](P --> Q) --> (<>P --> <>Q)" by S43_solve
-lemma "|- []P --> []<>P" by S43_solve
-lemma "|- <>[]P --> <>P" by S43_solve
+lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> (<>P \<longrightarrow> <>Q)" by S43_solve
+lemma "|- []P \<longrightarrow> []<>P" by S43_solve
+lemma "|- <>[]P \<longrightarrow> <>P" by S43_solve
-lemma "|- []P | []Q --> [](P | Q)" by S43_solve
-lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve
-lemma "|- [](P | Q) --> []P | <>Q" by S43_solve
-lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve
-lemma "|- [](P | Q) --> <>P | []Q" by S43_solve
+lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
+lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
+lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
(* Theorems of system S43 *)
-lemma "|- <>[]P --> []<>P" by S43_solve
-lemma "|- <>[]P --> [][]<>P" by S43_solve
-lemma "|- [](<>P | <>Q) --> []<>P | []<>Q" by S43_solve
-lemma "|- <>[]P & <>[]Q --> <>([]P & []Q)" by S43_solve
-lemma "|- []([]P --> []Q) | []([]Q --> []P)" by S43_solve
-lemma "|- [](<>P --> <>Q) | [](<>Q --> <>P)" by S43_solve
-lemma "|- []([]P --> Q) | []([]Q --> P)" by S43_solve
-lemma "|- [](P --> <>Q) | [](Q --> <>P)" by S43_solve
-lemma "|- [](P --> []Q-->R) | [](P | ([]R --> Q))" by S43_solve
-lemma "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)" by S43_solve
-lemma "|- []([]P | Q) & [](P | []Q) --> []P | []Q" by S43_solve
-lemma "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)" by S43_solve
-lemma "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q" by S43_solve
-lemma "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)" by S43_solve
-lemma "|- <>[]<>P <-> []<>P" by S43_solve
-lemma "|- []<>[]P <-> <>[]P" by S43_solve
+lemma "|- <>[]P \<longrightarrow> []<>P" by S43_solve
+lemma "|- <>[]P \<longrightarrow> [][]<>P" by S43_solve
+lemma "|- [](<>P \<or> <>Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve
+lemma "|- <>[]P \<and> <>[]Q \<longrightarrow> <>([]P \<and> []Q)" by S43_solve
+lemma "|- []([]P \<longrightarrow> []Q) \<or> []([]Q \<longrightarrow> []P)" by S43_solve
+lemma "|- [](<>P \<longrightarrow> <>Q) \<or> [](<>Q \<longrightarrow> <>P)" by S43_solve
+lemma "|- []([]P \<longrightarrow> Q) \<or> []([]Q \<longrightarrow> P)" by S43_solve
+lemma "|- [](P \<longrightarrow> <>Q) \<or> [](Q \<longrightarrow> <>P)" by S43_solve
+lemma "|- [](P \<longrightarrow> []Q \<longrightarrow> R) \<or> [](P \<or> ([]R \<longrightarrow> Q))" by S43_solve
+lemma "|- [](P \<or> (Q \<longrightarrow> <>C)) \<or> [](P \<longrightarrow> C \<longrightarrow> <>Q)" by S43_solve
+lemma "|- []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve
+lemma "|- <>P \<and> <>Q \<longrightarrow> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve
+lemma "|- [](P \<or> Q) \<and> []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve
+lemma "|- <>P \<and> <>Q \<longrightarrow> <>(P \<and> Q) \<or> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve
+lemma "|- <>[]<>P \<longleftrightarrow> []<>P" by S43_solve
+lemma "|- []<>[]P \<longleftrightarrow> <>[]P" by S43_solve
(* These are from Hailpern, LNCS 129 *)
-lemma "|- [](P & Q) <-> []P & []Q" by S43_solve
-lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve
-lemma "|- <>(P --> Q) <-> []P --> <>Q" by S43_solve
+lemma "|- [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
+lemma "|- <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
+lemma "|- <>(P \<longrightarrow> Q) \<longleftrightarrow> []P \<longrightarrow> <>Q" by S43_solve
-lemma "|- [](P --> Q) --> <>P --> <>Q" by S43_solve
-lemma "|- []P --> []<>P" by S43_solve
-lemma "|- <>[]P --> <>P" by S43_solve
-lemma "|- []<>[]P --> []<>P" by S43_solve
-lemma "|- <>[]P --> <>[]<>P" by S43_solve
-lemma "|- <>[]P --> []<>P" by S43_solve
-lemma "|- []<>[]P <-> <>[]P" by S43_solve
-lemma "|- <>[]<>P <-> []<>P" by S43_solve
+lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> <>P \<longrightarrow> <>Q" by S43_solve
+lemma "|- []P \<longrightarrow> []<>P" by S43_solve
+lemma "|- <>[]P \<longrightarrow> <>P" by S43_solve
+lemma "|- []<>[]P \<longrightarrow> []<>P" by S43_solve
+lemma "|- <>[]P \<longrightarrow> <>[]<>P" by S43_solve
+lemma "|- <>[]P \<longrightarrow> []<>P" by S43_solve
+lemma "|- []<>[]P \<longleftrightarrow> <>[]P" by S43_solve
+lemma "|- <>[]<>P \<longleftrightarrow> []<>P" by S43_solve
-lemma "|- []P | []Q --> [](P | Q)" by S43_solve
-lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve
-lemma "|- [](P | Q) --> []P | <>Q" by S43_solve
-lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve
-lemma "|- [](P | Q) --> <>P | []Q" by S43_solve
-lemma "|- [](P | Q) --> []<>P | []<>Q" by S43_solve
-lemma "|- <>[]P & <>[]Q --> <>(P & Q)" by S43_solve
-lemma "|- <>[](P & Q) <-> <>[]P & <>[]Q" by S43_solve
-lemma "|- []<>(P | Q) <-> []<>P | []<>Q" by S43_solve
+lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
+lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
+lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve
+lemma "|- <>[]P \<and> <>[]Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "|- <>[](P \<and> Q) \<longleftrightarrow> <>[]P \<and> <>[]Q" by S43_solve
+lemma "|- []<>(P \<or> Q) \<longleftrightarrow> []<>P \<or> []<>Q" by S43_solve
end
--- a/src/Sequents/Sequents.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/Sequents.thy Sat Oct 10 20:51:39 2015 +0200
@@ -19,9 +19,7 @@
subsection \<open>Sequences\<close>
-typedecl
- seq'
-
+typedecl seq'
consts
SeqO' :: "[o,seq']=>seq'"
Seq1' :: "o=>seq'"
@@ -149,4 +147,3 @@
ML_file "prover.ML"
end
-
--- a/src/Sequents/T.thy Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/T.thy Sat Oct 10 20:51:39 2015 +0200
@@ -13,22 +13,22 @@
(* delta * == {P | <>P : delta} *)
lstar0: "|L>" and
- lstar1: "$G |L> $H ==> []P, $G |L> P, $H" and
- lstar2: "$G |L> $H ==> P, $G |L> $H" and
+ lstar1: "$G |L> $H \<Longrightarrow> []P, $G |L> P, $H" and
+ lstar2: "$G |L> $H \<Longrightarrow> 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
+ rstar1: "$G |R> $H \<Longrightarrow> <>P, $G |R> P, $H" and
+ rstar2: "$G |R> $H \<Longrightarrow> 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" and
- boxL: "$E, P, $F |- $G ==> $E, []P, $F |- $G" and
- diaR: "$E |- $F, P, $G ==> $E |- $F, <>P, $G" and
+ "\<lbrakk>$E |L> $E'; $F |R> $F'; $G |R> $G';
+ $E' |- $F', P, $G'\<rbrakk> \<Longrightarrow> $E |- $F, []P, $G" and
+ boxL: "$E, P, $F |- $G \<Longrightarrow> $E, []P, $F |- $G" and
+ diaR: "$E |- $F, P, $G \<Longrightarrow> $E |- $F, <>P, $G" and
diaL:
- "[| $E |L> $E'; $F |L> $F'; $G |R> $G';
- $E', P, $F'|- $G'|] ==> $E, <>P, $F |- $G"
+ "\<lbrakk>$E |L> $E'; $F |L> $F'; $G |R> $G';
+ $E', P, $F'|- $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F |- $G"
ML \<open>
structure T_Prover = Modal_ProverFun
@@ -47,28 +47,28 @@
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
-lemma "|- []P --> P" by T_solve
-lemma "|- [](P-->Q) --> ([]P-->[]Q)" by T_solve (* normality*)
-lemma "|- (P--<Q) --> []P --> []Q" by T_solve
-lemma "|- P --> <>P" by T_solve
+lemma "|- []P \<longrightarrow> P" by T_solve
+lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by T_solve (* normality*)
+lemma "|- (P --< Q) \<longrightarrow> []P \<longrightarrow> []Q" by T_solve
+lemma "|- P \<longrightarrow> <>P" by T_solve
-lemma "|- [](P & Q) <-> []P & []Q" by T_solve
-lemma "|- <>(P | Q) <-> <>P | <>Q" by T_solve
-lemma "|- [](P<->Q) <-> (P>-<Q)" by T_solve
-lemma "|- <>(P-->Q) <-> ([]P--><>Q)" by T_solve
-lemma "|- []P <-> ~<>(~P)" by T_solve
-lemma "|- [](~P) <-> ~<>P" by T_solve
-lemma "|- ~[]P <-> <>(~P)" by T_solve
-lemma "|- [][]P <-> ~<><>(~P)" by T_solve
-lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by T_solve
+lemma "|- [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by T_solve
+lemma "|- <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by T_solve
+lemma "|- [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P >-< Q)" by T_solve
+lemma "|- <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by T_solve
+lemma "|- []P \<longleftrightarrow> \<not> <>(\<not> P)" by T_solve
+lemma "|- [](\<not> P) \<longleftrightarrow> \<not> <>P" by T_solve
+lemma "|- \<not> []P \<longleftrightarrow> <>(\<not> P)" by T_solve
+lemma "|- [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by T_solve
+lemma "|- \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>Q" by T_solve
-lemma "|- []P | []Q --> [](P | Q)" by T_solve
-lemma "|- <>(P & Q) --> <>P & <>Q" by T_solve
-lemma "|- [](P | Q) --> []P | <>Q" by T_solve
-lemma "|- <>P & []Q --> <>(P & Q)" by T_solve
-lemma "|- [](P | Q) --> <>P | []Q" by T_solve
-lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by T_solve
-lemma "|- (P--<Q) & (Q--<R) --> (P--<R)" by T_solve
-lemma "|- []P --> <>Q --> <>(P & Q)" by T_solve
+lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by T_solve
+lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by T_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by T_solve
+lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by T_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by T_solve
+lemma "|- <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by T_solve
+lemma "|- (P --< Q) \<and> (Q --< R ) \<longrightarrow> (P --< R)" by T_solve
+lemma "|- []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by T_solve
end