--- a/src/Sequents/ILL.thy Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/ILL.thy Sat Oct 10 20:54:44 2015 +0200
@@ -31,7 +31,7 @@
PromAux :: "three_seqi"
syntax
- "_Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
+ "_Trueprop" :: "single_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5)
"_Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5)
"_PromAux" :: "three_seqe" ("promaux {_||_||_}")
@@ -56,63 +56,63 @@
axiomatization where
-identity: "P |- P" and
+identity: "P \<turnstile> P" and
-zerol: "$G, 0, $H |- A" and
+zerol: "$G, 0, $H \<turnstile> A" and
(* RULES THAT DO NOT DIVIDE CONTEXT *)
-derelict: "$F, A, $G |- C \<Longrightarrow> $F, !A, $G |- C" and
+derelict: "$F, A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and
(* unfortunately, this one removes !A *)
-contract: "$F, !A, !A, $G |- C \<Longrightarrow> $F, !A, $G |- C" and
+contract: "$F, !A, !A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and
-weaken: "$F, $G |- C \<Longrightarrow> $G, !A, $F |- C" and
+weaken: "$F, $G \<turnstile> C \<Longrightarrow> $G, !A, $F \<turnstile> C" and
(* weak form of weakening, in practice just to clean context *)
(* weaken and contract not needed (CHECK) *)
-promote2: "promaux{ || $H || B} \<Longrightarrow> $H |- !B" and
+promote2: "promaux{ || $H || B} \<Longrightarrow> $H \<turnstile> !B" and
promote1: "promaux{!A, $G || $H || B}
\<Longrightarrow> promaux {$G || $H, !A || B}" and
-promote0: "$G |- A \<Longrightarrow> promaux {$G || || A}" and
+promote0: "$G \<turnstile> A \<Longrightarrow> promaux {$G || || A}" and
-tensl: "$H, A, B, $G |- C \<Longrightarrow> $H, A >< B, $G |- C" and
+tensl: "$H, A, B, $G \<turnstile> C \<Longrightarrow> $H, A >< B, $G \<turnstile> C" and
-impr: "A, $F |- B \<Longrightarrow> $F |- A -o B" and
+impr: "A, $F \<turnstile> B \<Longrightarrow> $F \<turnstile> A -o B" and
-conjr: "\<lbrakk>$F |- A ;
- $F |- B\<rbrakk>
- \<Longrightarrow> $F |- (A && B)" and
+conjr: "\<lbrakk>$F \<turnstile> A ;
+ $F \<turnstile> B\<rbrakk>
+ \<Longrightarrow> $F \<turnstile> (A && B)" and
-conjll: "$G, A, $H |- C \<Longrightarrow> $G, A && B, $H |- C" and
+conjll: "$G, A, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and
-conjlr: "$G, B, $H |- C \<Longrightarrow> $G, A && B, $H |- C" and
+conjlr: "$G, B, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> 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
+disjrl: "$G \<turnstile> A \<Longrightarrow> $G \<turnstile> A ++ B" and
+disjrr: "$G \<turnstile> B \<Longrightarrow> $G \<turnstile> A ++ B" and
+disjl: "\<lbrakk>$G, A, $H \<turnstile> C ;
+ $G, B, $H \<turnstile> C\<rbrakk>
+ \<Longrightarrow> $G, A ++ B, $H \<turnstile> C" and
(* RULES THAT DIVIDE CONTEXT *)
tensr: "\<lbrakk>$F, $J :=: $G;
- $F |- A ;
- $J |- B\<rbrakk>
- \<Longrightarrow> $G |- A >< B" and
+ $F \<turnstile> A ;
+ $J \<turnstile> B\<rbrakk>
+ \<Longrightarrow> $G \<turnstile> A >< B" and
impl: "\<lbrakk>$G, $F :=: $J, $H ;
- B, $F |- C ;
- $G |- A\<rbrakk>
- \<Longrightarrow> $J, A -o B, $H |- C" and
+ B, $F \<turnstile> C ;
+ $G \<turnstile> A\<rbrakk>
+ \<Longrightarrow> $J, A -o B, $H \<turnstile> C" 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
+ $H1, $H2, $H3, $H4 \<turnstile> A ;
+ $J1, $J2, A, $J3, $J4 \<turnstile> B\<rbrakk> \<Longrightarrow> $F \<turnstile> B" and
(* CONTEXT RULES *)
@@ -150,7 +150,7 @@
zerol
identity
-lemma aux_impl: "$F, $G |- A \<Longrightarrow> $F, !(A -o B), $G |- B"
+lemma aux_impl: "$F, $G \<turnstile> A \<Longrightarrow> $F, !(A -o B), $G \<turnstile> B"
apply (rule derelict)
apply (rule impl)
apply (rule_tac [2] identity)
@@ -158,16 +158,16 @@
apply assumption
done
-lemma conj_lemma: " $F, !A, !B, $G |- C \<Longrightarrow> $F, !(A && B), $G |- C"
+lemma conj_lemma: " $F, !A, !B, $G \<turnstile> C \<Longrightarrow> $F, !(A && B), $G \<turnstile> C"
apply (rule contract)
apply (rule_tac A = " (!A) >< (!B) " in cut)
apply (rule_tac [2] tensr)
prefer 3
- apply (subgoal_tac "! (A && B) |- !A")
+ apply (subgoal_tac "! (A && B) \<turnstile> !A")
apply assumption
apply best
prefer 3
- apply (subgoal_tac "! (A && B) |- !B")
+ apply (subgoal_tac "! (A && B) \<turnstile> !B")
apply assumption
apply best
apply (rule_tac [2] context1)
@@ -178,20 +178,20 @@
apply (rule context1)
done
-lemma impr_contract: "!A, !A, $G |- B \<Longrightarrow> $G |- (!A) -o B"
+lemma impr_contract: "!A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!A) -o B"
apply (rule impr)
apply (rule contract)
apply assumption
done
-lemma impr_contr_der: "A, !A, $G |- B \<Longrightarrow> $G |- (!A) -o B"
+lemma impr_contr_der: "A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!A) -o B"
apply (rule impr)
apply (rule contract)
apply (rule derelict)
apply assumption
done
-lemma contrad1: "$F, (!B) -o 0, $G, !B, $H |- A"
+lemma contrad1: "$F, (!B) -o 0, $G, !B, $H \<turnstile> A"
apply (rule impl)
apply (rule_tac [3] identity)
apply (rule context3)
@@ -200,7 +200,7 @@
done
-lemma contrad2: "$F, !B, $G, (!B) -o 0, $H |- A"
+lemma contrad2: "$F, !B, $G, (!B) -o 0, $H \<turnstile> A"
apply (rule impl)
apply (rule_tac [3] identity)
apply (rule context3)
@@ -208,14 +208,14 @@
apply (rule zerol)
done
-lemma ll_mp: "A -o B, A |- B"
+lemma ll_mp: "A -o B, A \<turnstile> B"
apply (rule impl)
apply (rule_tac [2] identity)
apply (rule_tac [2] identity)
apply (rule context1)
done
-lemma mp_rule1: "$F, B, $G, $H |- C \<Longrightarrow> $F, A, $G, A -o B, $H |- C"
+lemma mp_rule1: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A, $G, A -o B, $H \<turnstile> C"
apply (rule_tac A = "B" in cut)
apply (rule_tac [2] ll_mp)
prefer 2 apply (assumption)
@@ -224,7 +224,7 @@
apply (rule context1)
done
-lemma mp_rule2: "$F, B, $G, $H |- C \<Longrightarrow> $F, A -o B, $G, A, $H |- C"
+lemma mp_rule2: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A -o B, $G, A, $H \<turnstile> C"
apply (rule_tac A = "B" in cut)
apply (rule_tac [2] ll_mp)
prefer 2 apply (assumption)
@@ -233,11 +233,11 @@
apply (rule context1)
done
-lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
+lemma or_to_and: "!((!(A ++ B)) -o 0) \<turnstile> !( ((!A) -o 0) && ((!B) -o 0))"
by best
-lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C \<Longrightarrow>
- $F, !((!(A ++ B)) -o 0), $G |- C"
+lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G \<turnstile> C \<Longrightarrow>
+ $F, !((!(A ++ B)) -o 0), $G \<turnstile> C"
apply (rule cut)
apply (rule_tac [2] or_to_and)
prefer 2 apply (assumption)
@@ -245,17 +245,17 @@
apply (rule context1)
done
-lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
+lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) \<turnstile> (!(A && B)) -o C"
apply (rule impr)
apply (rule conj_lemma)
apply (rule disjl)
apply (rule mp_rule1, best)+
done
-lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0"
+lemma not_imp: "!A, !((!B) -o 0) \<turnstile> (!((!A) -o B)) -o 0"
by best
-lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0"
+lemma a_not_a: "!A -o (!A -o 0) \<turnstile> !A -o 0"
apply (rule impr)
apply (rule contract)
apply (rule impl)
@@ -264,7 +264,7 @@
apply best
done
-lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B \<Longrightarrow> $J1, !A -o (!A -o 0), $J2 |- B"
+lemma a_not_a_rule: "$J1, !A -o 0, $J2 \<turnstile> B \<Longrightarrow> $J1, !A -o (!A -o 0), $J2 \<turnstile> B"
apply (rule_tac A = "!A -o 0" in cut)
apply (rule_tac [2] a_not_a)
prefer 2 apply assumption
@@ -294,17 +294,17 @@
(* Some examples from Troelstra and van Dalen *)
-lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0"
+lemma "!((!A) -o ((!B) -o 0)) \<turnstile> (!(A && B)) -o 0"
by best_safe
-lemma "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))"
+lemma "!((!(A && B)) -o 0) \<turnstile> !((!A) -o ((!B) -o 0))"
by best_safe
-lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |-
+lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) \<turnstile>
(!A) -o ( (! ((!B) -o 0)) -o 0)"
by best_safe
-lemma "!( (!A) -o ( (! ((!B) -o 0)) -o 0) ) |-
+lemma "!( (!A) -o ( (! ((!B) -o 0)) -o 0) ) \<turnstile>
(!((! ((!A) -o B) ) -o 0)) -o 0"
by best_power
--- a/src/Sequents/ILL_predlog.thy Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/ILL_predlog.thy Sat Oct 10 20:54:44 2015 +0200
@@ -30,100 +30,100 @@
(* from [kleene 52] pp 118,119 *)
-lemma k49a: "|- [* A > ( - ( - A)) *]"
+lemma k49a: "\<turnstile> [* A > ( - ( - A)) *]"
by best_safe
-lemma k49b: "|- [*( - ( - ( - A))) = ( - A)*]"
+lemma k49b: "\<turnstile> [*( - ( - ( - A))) = ( - A)*]"
by best_safe
-lemma k49c: "|- [* (A | - A) > ( - - A = A) *]"
+lemma k49c: "\<turnstile> [* (A | - A) > ( - - A = A) *]"
by best_safe
-lemma k50a: "|- [* - (A = - A) *]"
+lemma k50a: "\<turnstile> [* - (A = - A) *]"
by best_power
-lemma k51a: "|- [* - - (A | - A) *]"
+lemma k51a: "\<turnstile> [* - - (A | - A) *]"
by best_safe
-lemma k51b: "|- [* - - (- - A > A) *]"
+lemma k51b: "\<turnstile> [* - - (- - A > A) *]"
by best_power
-lemma k56a: "|- [* (A | B) > - (- A & - B) *]"
+lemma k56a: "\<turnstile> [* (A | B) > - (- A & - B) *]"
by best_safe
-lemma k56b: "|- [* (-A | B) > - (A & -B) *]"
+lemma k56b: "\<turnstile> [* (-A | B) > - (A & -B) *]"
by best_safe
-lemma k57a: "|- [* (A & B) > - (-A | -B) *]"
+lemma k57a: "\<turnstile> [* (A & B) > - (-A | -B) *]"
by best_safe
-lemma k57b: "|- [* (A & -B) > -(-A | B) *]"
+lemma k57b: "\<turnstile> [* (A & -B) > -(-A | B) *]"
by best_power
-lemma k58a: "|- [* (A > B) > - (A & -B) *]"
+lemma k58a: "\<turnstile> [* (A > B) > - (A & -B) *]"
by best_safe
-lemma k58b: "|- [* (A > -B) = -(A & B) *]"
+lemma k58b: "\<turnstile> [* (A > -B) = -(A & B) *]"
by best_safe
-lemma k58c: "|- [* - (A & B) = (- - A > - B) *]"
+lemma k58c: "\<turnstile> [* - (A & B) = (- - A > - B) *]"
by best_safe
-lemma k58d: "|- [* (- - A > - B) = - - (-A | -B) *]"
+lemma k58d: "\<turnstile> [* (- - A > - B) = - - (-A | -B) *]"
by best_safe
-lemma k58e: "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]"
+lemma k58e: "! [* - -B > B *] \<turnstile> [* (- -A > B) = (A > B) *]"
by best_safe
-lemma k58f: "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]"
+lemma k58f: "! [* - -B > B *] \<turnstile> [* (A > B) = - (A & -B) *]"
by best_safe
-lemma k58g: "|- [* (- -A > B) > - (A & -B) *]"
+lemma k58g: "\<turnstile> [* (- -A > B) > - (A & -B) *]"
by best_safe
-lemma k59a: "|- [* (-A | B) > (A > B) *]"
+lemma k59a: "\<turnstile> [* (-A | B) > (A > B) *]"
by best_safe
-lemma k59b: "|- [* (A > B) > - - (-A | B) *]"
+lemma k59b: "\<turnstile> [* (A > B) > - - (-A | B) *]"
by best_power
-lemma k59c: "|- [* (-A > B) > - -(A | B) *]"
+lemma k59c: "\<turnstile> [* (-A > B) > - -(A | B) *]"
by best_power
-lemma k60a: "|- [* (A & B) > - (A > -B) *]"
+lemma k60a: "\<turnstile> [* (A & B) > - (A > -B) *]"
by best_safe
-lemma k60b: "|- [* (A & -B) > - (A > B) *]"
+lemma k60b: "\<turnstile> [* (A & -B) > - (A > B) *]"
by best_safe
-lemma k60c: "|- [* ( - - A & B) > - (A > -B) *]"
+lemma k60c: "\<turnstile> [* ( - - A & B) > - (A > -B) *]"
by best_safe
-lemma k60d: "|- [* (- - A & - B) = - (A > B) *]"
+lemma k60d: "\<turnstile> [* (- - A & - B) = - (A > B) *]"
by best_safe
-lemma k60e: "|- [* - (A > B) = - (-A | B) *]"
+lemma k60e: "\<turnstile> [* - (A > B) = - (-A | B) *]"
by best_safe
-lemma k60f: "|- [* - (-A | B) = - - (A & -B) *]"
+lemma k60f: "\<turnstile> [* - (-A | B) = - - (A & -B) *]"
by best_safe
-lemma k60g: "|- [* - - (A > B) = - (A & -B) *]"
+lemma k60g: "\<turnstile> [* - - (A > B) = - (A & -B) *]"
by best_power
-lemma k60h: "|- [* - (A & -B) = (A > - -B) *]"
+lemma k60h: "\<turnstile> [* - (A & -B) = (A > - -B) *]"
by best_safe
-lemma k60i: "|- [* (A > - -B) = (- -A > - -B) *]"
+lemma k60i: "\<turnstile> [* (A > - -B) = (- -A > - -B) *]"
by best_safe
-lemma k61a: "|- [* (A | B) > (-A > B) *]"
+lemma k61a: "\<turnstile> [* (A | B) > (-A > B) *]"
by best_safe
-lemma k61b: "|- [* - (A | B) = - (-A > B) *]"
+lemma k61b: "\<turnstile> [* - (A | B) = - (-A > B) *]"
by best_power
-lemma k62a: "|- [* (-A | -B) > - (A & B) *]"
+lemma k62a: "\<turnstile> [* (-A | -B) > - (A & B) *]"
by best_safe
end
--- a/src/Sequents/LK.thy Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/LK.thy Sat Oct 10 20:54:44 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 \<Longrightarrow>, needed for instance to prove imp_cong.
+link between \<turnstile> 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,65 +17,65 @@
begin
axiomatization where
- monotonic: "($H |- P \<Longrightarrow> $H |- Q) \<Longrightarrow> $H, P |- Q" and
+ monotonic: "($H \<turnstile> P \<Longrightarrow> $H \<turnstile> Q) \<Longrightarrow> $H, P \<turnstile> Q" and
- left_cong: "\<lbrakk>P == P'; |- P' \<Longrightarrow> ($H |- $F) \<equiv> ($H' |- $F')\<rbrakk>
- \<Longrightarrow> (P, $H |- $F) \<equiv> (P', $H' |- $F')"
+ left_cong: "\<lbrakk>P == P'; \<turnstile> P' \<Longrightarrow> ($H \<turnstile> $F) \<equiv> ($H' \<turnstile> $F')\<rbrakk>
+ \<Longrightarrow> (P, $H \<turnstile> $F) \<equiv> (P', $H' \<turnstile> $F')"
subsection \<open>Rewrite rules\<close>
lemma conj_simps:
- "|- 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)"
+ "\<turnstile> P \<and> True \<longleftrightarrow> P"
+ "\<turnstile> True \<and> P \<longleftrightarrow> P"
+ "\<turnstile> P \<and> False \<longleftrightarrow> False"
+ "\<turnstile> False \<and> P \<longleftrightarrow> False"
+ "\<turnstile> P \<and> P \<longleftrightarrow> P"
+ "\<turnstile> P \<and> P \<and> Q \<longleftrightarrow> P \<and> Q"
+ "\<turnstile> P \<and> \<not> P \<longleftrightarrow> False"
+ "\<turnstile> \<not> P \<and> P \<longleftrightarrow> False"
+ "\<turnstile> (P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
by (fast add!: subst)+
lemma disj_simps:
- "|- 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)"
+ "\<turnstile> P \<or> True \<longleftrightarrow> True"
+ "\<turnstile> True \<or> P \<longleftrightarrow> True"
+ "\<turnstile> P \<or> False \<longleftrightarrow> P"
+ "\<turnstile> False \<or> P \<longleftrightarrow> P"
+ "\<turnstile> P \<or> P \<longleftrightarrow> P"
+ "\<turnstile> P \<or> P \<or> Q \<longleftrightarrow> P \<or> Q"
+ "\<turnstile> (P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
by (fast add!: subst)+
lemma not_simps:
- "|- \<not> False \<longleftrightarrow> True"
- "|- \<not> True \<longleftrightarrow> False"
+ "\<turnstile> \<not> False \<longleftrightarrow> True"
+ "\<turnstile> \<not> True \<longleftrightarrow> False"
by (fast add!: subst)+
lemma imp_simps:
- "|- (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"
+ "\<turnstile> (P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
+ "\<turnstile> (P \<longrightarrow> True) \<longleftrightarrow> True"
+ "\<turnstile> (False \<longrightarrow> P) \<longleftrightarrow> True"
+ "\<turnstile> (True \<longrightarrow> P) \<longleftrightarrow> P"
+ "\<turnstile> (P \<longrightarrow> P) \<longleftrightarrow> True"
+ "\<turnstile> (P \<longrightarrow> \<not> P) \<longleftrightarrow> \<not> P"
by (fast add!: subst)+
lemma iff_simps:
- "|- (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"
+ "\<turnstile> (True \<longleftrightarrow> P) \<longleftrightarrow> P"
+ "\<turnstile> (P \<longleftrightarrow> True) \<longleftrightarrow> P"
+ "\<turnstile> (P \<longleftrightarrow> P) \<longleftrightarrow> True"
+ "\<turnstile> (False \<longleftrightarrow> P) \<longleftrightarrow> \<not> P"
+ "\<turnstile> (P \<longleftrightarrow> False) \<longleftrightarrow> \<not> P"
by (fast add!: subst)+
lemma quant_simps:
- "\<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)"
+ "\<And>P. \<turnstile> (\<forall>x. P) \<longleftrightarrow> P"
+ "\<And>P. \<turnstile> (\<forall>x. x = t \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
+ "\<And>P. \<turnstile> (\<forall>x. t = x \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
+ "\<And>P. \<turnstile> (\<exists>x. P) \<longleftrightarrow> P"
+ "\<And>P. \<turnstile> (\<exists>x. x = t \<and> P(x)) \<longleftrightarrow> P(t)"
+ "\<And>P. \<turnstile> (\<exists>x. t = x \<and> P(x)) \<longleftrightarrow> P(t)"
by (fast add!: subst)+
@@ -89,39 +89,39 @@
text \<open>existential miniscoping\<close>
lemma ex_simps:
- "\<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))"
+ "\<And>P Q. \<turnstile> (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
+ "\<And>P Q. \<turnstile> (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
+ "\<And>P Q. \<turnstile> (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
+ "\<And>P Q. \<turnstile> (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
+ "\<And>P Q. \<turnstile> (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+ "\<And>P Q. \<turnstile> (\<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:
- "\<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))"
+ "\<And>P Q. \<turnstile> (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
+ "\<And>P Q. \<turnstile> (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
+ "\<And>P Q. \<turnstile> (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<longrightarrow> Q"
+ "\<And>P Q. \<turnstile> (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))"
+ "\<And>P Q. \<turnstile> (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
+ "\<And>P Q. \<turnstile> (\<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 \<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)"
+ "\<turnstile> P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R"
+ "\<turnstile> (Q \<or> R) \<and> P \<longleftrightarrow> Q \<and> P \<or> R \<and> P"
+ "\<turnstile> (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
by (fast add!: subst)+
-lemma P_iff_F: "|- \<not> P \<Longrightarrow> |- (P \<longleftrightarrow> False)"
+lemma P_iff_F: "\<turnstile> \<not> P \<Longrightarrow> \<turnstile> (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 \<Longrightarrow> |- (P \<longleftrightarrow> True)"
+lemma P_iff_T: "\<turnstile> P \<Longrightarrow> \<turnstile> (P \<longleftrightarrow> True)"
apply (erule thinR [THEN cut])
apply fast
done
@@ -130,51 +130,51 @@
lemma LK_extra_simps:
- "|- 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)"
+ "\<turnstile> P \<or> \<not> P"
+ "\<turnstile> \<not> P \<or> P"
+ "\<turnstile> \<not> \<not> P \<longleftrightarrow> P"
+ "\<turnstile> (\<not> P \<longrightarrow> P) \<longleftrightarrow> P"
+ "\<turnstile> (\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)"
by (fast add!: subst)+
subsection \<open>Named rewrite rules\<close>
-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)"
+lemma conj_commute: "\<turnstile> P \<and> Q \<longleftrightarrow> Q \<and> P"
+ and conj_left_commute: "\<turnstile> 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 \<or> Q \<longleftrightarrow> Q \<or> P"
- and disj_left_commute: "|- P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)"
+lemma disj_commute: "\<turnstile> P \<or> Q \<longleftrightarrow> Q \<or> P"
+ and disj_left_commute: "\<turnstile> 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 \<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)"
+lemma conj_disj_distribL: "\<turnstile> P \<and> (Q \<or> R) \<longleftrightarrow> (P \<and> Q \<or> P \<and> R)"
+ and conj_disj_distribR: "\<turnstile> (P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R \<or> Q \<and> 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 disj_conj_distribL: "\<turnstile> P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
+ and disj_conj_distribR: "\<turnstile> (P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> 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_conj_distrib: "\<turnstile> (P \<longrightarrow> (Q \<and> R)) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
+ and imp_conj: "\<turnstile> ((P \<and> Q) \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
+ and imp_disj: "\<turnstile> (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> 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 imp_disj1: "\<turnstile> (P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
+ and imp_disj2: "\<turnstile> Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
- 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 de_Morgan_disj: "\<turnstile> (\<not> (P \<or> Q)) \<longleftrightarrow> (\<not> P \<and> \<not> Q)"
+ and de_Morgan_conj: "\<turnstile> (\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)"
- and not_iff: "|- \<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)"
+ and not_iff: "\<turnstile> \<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)"
by (fast add!: subst)+
lemma imp_cong:
- assumes p1: "|- P \<longleftrightarrow> P'"
- and p2: "|- P' \<Longrightarrow> |- Q \<longleftrightarrow> Q'"
- shows "|- (P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q')"
+ assumes p1: "\<turnstile> P \<longleftrightarrow> P'"
+ and p2: "\<turnstile> P' \<Longrightarrow> \<turnstile> Q \<longleftrightarrow> Q'"
+ shows "\<turnstile> (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 \<longleftrightarrow> P'"
- and p2: "|- P' \<Longrightarrow> |- Q \<longleftrightarrow> Q'"
- shows "|- (P \<and> Q) \<longleftrightarrow> (P' \<and> Q')"
+ assumes p1: "\<turnstile> P \<longleftrightarrow> P'"
+ and p2: "\<turnstile> P' \<Longrightarrow> \<turnstile> Q \<longleftrightarrow> Q'"
+ shows "\<turnstile> (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 \<longleftrightarrow> y = x"
+lemma eq_sym_conv: "\<turnstile> x = y \<longleftrightarrow> y = x"
by (fast add!: subst)
ML_file "simpdata.ML"
@@ -207,10 +207,10 @@
text \<open>To create substition rules\<close>
-lemma eq_imp_subst: "|- a = b \<Longrightarrow> $H, A(a), $G |- $E, A(b), $F"
+lemma eq_imp_subst: "\<turnstile> a = b \<Longrightarrow> $H, A(a), $G \<turnstile> $E, A(b), $F"
by simp
-lemma split_if: "|- P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) \<and> (\<not> Q \<longrightarrow> P(y)))"
+lemma split_if: "\<turnstile> 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)
@@ -220,12 +220,12 @@
apply fast
done
-lemma if_cancel: "|- (if P then x else x) = x"
+lemma if_cancel: "\<turnstile> (if P then x else x) = x"
apply (lem split_if)
apply fast
done
-lemma if_eq_cancel: "|- (if x = y then y else x) = x"
+lemma if_eq_cancel: "\<turnstile> (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 20:51:39 2015 +0200
+++ b/src/Sequents/LK/Hard_Quantifiers.thy Sat Oct 10 20:54:44 2015 +0200
@@ -15,68 +15,68 @@
imports "../LK"
begin
-lemma "|- (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
+lemma "\<turnstile> (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
by fast
-lemma "|- (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
+lemma "\<turnstile> (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
by fast
-lemma "|- (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+lemma "\<turnstile> (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
by fast
-lemma "|- (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
+lemma "\<turnstile> (\<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 \<forall>*)
-lemma "|- (\<forall>x. P(x) \<longrightarrow> P(f(x))) \<and> P(d) \<longrightarrow> P(f(f(f(d))))"
+lemma "\<turnstile> (\<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 "|- \<exists>x. P(x) \<longrightarrow> P(a) \<and> P(b)"
+lemma "\<turnstile> \<exists>x. P(x) \<longrightarrow> P(a) \<and> P(b)"
by fast_dup
-lemma "|- \<exists>z. P(z) \<longrightarrow> (\<forall>x. P(x))"
+lemma "\<turnstile> \<exists>z. P(z) \<longrightarrow> (\<forall>x. P(x))"
by best_dup
text "Hard examples with quantifiers"
text "Problem 18"
-lemma "|- \<exists>y. \<forall>x. P(y)\<longrightarrow>P(x)"
+lemma "\<turnstile> \<exists>y. \<forall>x. P(y)\<longrightarrow>P(x)"
by best_dup
text "Problem 19"
-lemma "|- \<exists>x. \<forall>y z. (P(y)\<longrightarrow>Q(z)) \<longrightarrow> (P(x)\<longrightarrow>Q(x))"
+lemma "\<turnstile> \<exists>x. \<forall>y z. (P(y)\<longrightarrow>Q(z)) \<longrightarrow> (P(x)\<longrightarrow>Q(x))"
by best_dup
text "Problem 20"
-lemma "|- (\<forall>x y. \<exists>z. \<forall>w. (P(x) \<and> Q(y)\<longrightarrow>R(z) \<and> S(w)))
+lemma "\<turnstile> (\<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 "|- (\<exists>x. P \<longrightarrow> Q(x)) \<and> (\<exists>x. Q(x) \<longrightarrow> P) \<longrightarrow> (\<exists>x. P \<longleftrightarrow> Q(x))"
+lemma "\<turnstile> (\<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 "|- (\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))"
+lemma "\<turnstile> (\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))"
by fast
text "Problem 23"
-lemma "|- (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x)))"
+lemma "\<turnstile> (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x)))"
by best
text "Problem 24"
-lemma "|- \<not> (\<exists>x. S(x) \<and> Q(x)) \<and> (\<forall>x. P(x) \<longrightarrow> Q(x) \<or> R(x)) \<and>
+lemma "\<turnstile> \<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 "|- (\<exists>x. P(x)) \<and>
+lemma "\<turnstile> (\<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)))
@@ -84,13 +84,13 @@
by best
text "Problem 26"
-lemma "|- ((\<exists>x. p(x)) \<longleftrightarrow> (\<exists>x. q(x))) \<and>
+lemma "\<turnstile> ((\<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 "|- (\<exists>x. P(x) \<and> \<not> Q(x)) \<and>
+lemma "\<turnstile> (\<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)))
@@ -98,57 +98,57 @@
by pc
text "Problem 28. AMENDED"
-lemma "|- (\<forall>x. P(x) \<longrightarrow> (\<forall>x. Q(x))) \<and>
+lemma "\<turnstile> (\<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 "|- (\<exists>x. P(x)) \<and> (\<exists>y. Q(y))
+lemma "\<turnstile> (\<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 "|- (\<forall>x. P(x) \<or> Q(x) \<longrightarrow> \<not> R(x)) \<and>
+lemma "\<turnstile> (\<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 "|- \<not> (\<exists>x. P(x) \<and> (Q(x) \<or> R(x))) \<and>
+lemma "\<turnstile> \<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 "|- (\<forall>x. P(x) \<and> (Q(x) \<or> R(x)) \<longrightarrow> S(x)) \<and>
+lemma "\<turnstile> (\<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 "|- (\<forall>x. P(a) \<and> (P(x) \<longrightarrow> P(b)) \<longrightarrow> P(c)) \<longleftrightarrow>
+lemma "\<turnstile> (\<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 "|- ((\<exists>x. \<forall>y. p(x) \<longleftrightarrow> p(y)) \<longleftrightarrow>
+lemma "\<turnstile> ((\<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 "|- \<exists>x y. P(x,y) \<longrightarrow> (\<forall>u v. P(u,v))"
+lemma "\<turnstile> \<exists>x y. P(x,y) \<longrightarrow> (\<forall>u v. P(u,v))"
by best_dup
text "Problem 36"
-lemma "|- (\<forall>x. \<exists>y. J(x,y)) \<and>
+lemma "\<turnstile> (\<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)))
@@ -156,7 +156,7 @@
by fast
text "Problem 37"
-lemma "|- (\<forall>z. \<exists>w. \<forall>x. \<exists>y.
+lemma "\<turnstile> (\<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)))
@@ -164,7 +164,7 @@
by pc
text "Problem 38"
-lemma "|- (\<forall>x. p(a) \<and> (p(x) \<longrightarrow> (\<exists>y. p(y) \<and> r(x,y))) \<longrightarrow>
+lemma "\<turnstile> (\<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>
@@ -172,37 +172,37 @@
by pc
text "Problem 39"
-lemma "|- \<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))"
+lemma "\<turnstile> \<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))"
by fast
text "Problem 40. AMENDED"
-lemma "|- (\<exists>y. \<forall>x. F(x,y) \<longleftrightarrow> F(x,x)) \<longrightarrow>
+lemma "\<turnstile> (\<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 "|- (\<forall>z. \<exists>y. \<forall>x. f(x,y) \<longleftrightarrow> f(x,z) \<and> \<not> f(x,x))
+lemma "\<turnstile> (\<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 "|- \<not> (\<exists>y. \<forall>x. p(x,y) \<longleftrightarrow> \<not> (\<exists>z. p(x,z) \<and> p(z,x)))"
+lemma "\<turnstile> \<not> (\<exists>y. \<forall>x. p(x,y) \<longleftrightarrow> \<not> (\<exists>z. p(x,z) \<and> p(z,x)))"
oops
text "Problem 43"
-lemma "|- (\<forall>x. \<forall>y. q(x,y) \<longleftrightarrow> (\<forall>z. p(z,x) \<longleftrightarrow> p(z,y)))
+lemma "\<turnstile> (\<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 "|- (\<forall>x. f(x) \<longrightarrow>
+lemma "\<turnstile> (\<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 "|- (\<forall>x. f(x) \<and> (\<forall>y. g(y) \<and> h(x,y) \<longrightarrow> j(x,y))
+lemma "\<turnstile> (\<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))
@@ -214,50 +214,50 @@
text "Problems (mainly) involving equality or functions"
text "Problem 48"
-lemma "|- (a = b \<or> c = d) \<and> (a = c \<or> b = d) \<longrightarrow> a = d \<or> b = c"
+lemma "\<turnstile> (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 "|- (\<forall>x. P(a,x) \<or> (\<forall>y. P(x,y))) \<longrightarrow> (\<exists>x. \<forall>y. P(x,y))"
+lemma "\<turnstile> (\<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 "|- (\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+lemma "\<turnstile> (\<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 "|- (\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+lemma "\<turnstile> (\<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 "|- (\<forall>x.(\<exists>y. P(y) \<and> x = f(y)) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> P(f(x)))"
+lemma "\<turnstile> (\<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)) \<and> P(f(b,c), f(a,c)) \<and>
+lemma "\<turnstile> 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 "|- (\<forall>x y. f(x) = g(y)) \<longrightarrow> (\<forall>x y. f(f(x)) = f(g(y)))"
+lemma "\<turnstile> (\<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 "|- (\<forall>x. P(x) \<longleftrightarrow> \<not> P(f(x))) \<longrightarrow> (\<exists>x. P(x) \<and> \<not> P(f(x)))"
+lemma "\<turnstile> (\<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 "|- \<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))"
+lemma "\<turnstile> \<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 "|- (\<forall>x. p(a) \<and> (p(x) \<longrightarrow> p(f(x))) \<longrightarrow> p(f(f(x)))) \<longleftrightarrow>
+lemma "\<turnstile> (\<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
--- a/src/Sequents/LK/Nat.thy Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/LK/Nat.thy Sat Oct 10 20:54:44 2015 +0200
@@ -17,13 +17,13 @@
Suc :: "nat \<Rightarrow> nat" and
rec :: "[nat, 'a, [nat,'a] \<Rightarrow> 'a] \<Rightarrow> 'a"
where
- 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
+ induct: "\<lbrakk>$H \<turnstile> $E, P(0), $F;
+ \<And>x. $H, P(x) \<turnstile> $E, P(Suc(x)), $F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P(n), $F" 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))"
+ Suc_inject: "\<turnstile> Suc(m) = Suc(n) \<longrightarrow> m = n" and
+ Suc_neq_0: "\<turnstile> Suc(m) \<noteq> 0" and
+ rec_0: "\<turnstile> rec(0,a,f) = a" and
+ rec_Suc: "\<turnstile> rec(Suc(m), a, f) = f(m, rec(m,a,f))"
definition add :: "[nat, nat] \<Rightarrow> nat" (infixl "+" 60)
where "m + n == rec(m, n, \<lambda>x y. Suc(y))"
@@ -31,43 +31,43 @@
declare Suc_neq_0 [simp]
-lemma Suc_inject_rule: "$H, $G, m = n |- $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G |- $E"
+lemma Suc_inject_rule: "$H, $G, m = n \<turnstile> $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G \<turnstile> $E"
by (rule L_of_imp [OF Suc_inject])
-lemma Suc_n_not_n: "|- Suc(k) \<noteq> k"
+lemma Suc_n_not_n: "\<turnstile> 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: "\<turnstile> 0 + n = n"
apply (unfold add_def)
apply (rule rec_0)
done
-lemma add_Suc: "|- Suc(m) + n = Suc(m + n)"
+lemma add_Suc: "\<turnstile> 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: "\<turnstile> (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: "\<turnstile> 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: "\<turnstile> m + Suc(n) = Suc(m + n)"
apply (rule_tac n = "m" in induct)
apply simp_all
done
-lemma "(\<And>n. |- f(Suc(n)) = Suc(f(n))) \<Longrightarrow> |- f(i + j) = i + f(j)"
+lemma "(\<And>n. \<turnstile> f(Suc(n)) = Suc(f(n))) \<Longrightarrow> \<turnstile> 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 20:51:39 2015 +0200
+++ b/src/Sequents/LK/Propositional.thy Sat Oct 10 20:54:44 2015 +0200
@@ -11,73 +11,73 @@
text "absorptive laws of \<and> and \<or>"
-lemma "|- P \<and> P \<longleftrightarrow> P"
+lemma "\<turnstile> P \<and> P \<longleftrightarrow> P"
by fast_prop
-lemma "|- P \<or> P \<longleftrightarrow> P"
+lemma "\<turnstile> P \<or> P \<longleftrightarrow> P"
by fast_prop
text "commutative laws of \<and> and \<or>"
-lemma "|- P \<and> Q \<longleftrightarrow> Q \<and> P"
+lemma "\<turnstile> P \<and> Q \<longleftrightarrow> Q \<and> P"
by fast_prop
-lemma "|- P \<or> Q \<longleftrightarrow> Q \<or> P"
+lemma "\<turnstile> P \<or> Q \<longleftrightarrow> Q \<or> P"
by fast_prop
text "associative laws of \<and> and \<or>"
-lemma "|- (P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
+lemma "\<turnstile> (P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
by fast_prop
-lemma "|- (P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
+lemma "\<turnstile> (P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
by fast_prop
text "distributive laws of \<and> and \<or>"
-lemma "|- (P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)"
+lemma "\<turnstile> (P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)"
by fast_prop
-lemma "|- (P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R) \<or> (Q \<and> R)"
+lemma "\<turnstile> (P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R) \<or> (Q \<and> R)"
by fast_prop
text "Laws involving implication"
-lemma "|- (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
+lemma "\<turnstile> (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
by fast_prop
-lemma "|- (P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
+lemma "\<turnstile> (P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
by fast_prop
-lemma "|- (P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
+lemma "\<turnstile> (P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
by fast_prop
text "Classical theorems"
-lemma "|- P \<or> Q \<longrightarrow> P \<or> \<not> P \<and> Q"
+lemma "\<turnstile> P \<or> Q \<longrightarrow> P \<or> \<not> P \<and> Q"
by fast_prop
-lemma "|- (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<or> R)"
+lemma "\<turnstile> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<or> R)"
by fast_prop
-lemma "|- P \<and> Q \<or> \<not> P \<and> R \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R)"
+lemma "\<turnstile> P \<and> Q \<or> \<not> P \<and> R \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R)"
by fast_prop
-lemma "|- (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
+lemma "\<turnstile> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
by fast_prop
(*If and only if*)
-lemma "|- (P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
+lemma "\<turnstile> (P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
by fast_prop
-lemma "|- \<not> (P \<longleftrightarrow> \<not> P)"
+lemma "\<turnstile> \<not> (P \<longleftrightarrow> \<not> P)"
by fast_prop
@@ -89,71 +89,71 @@
*)
(*1*)
-lemma "|- (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
+lemma "\<turnstile> (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
by fast_prop
(*2*)
-lemma "|- \<not> \<not> P \<longleftrightarrow> P"
+lemma "\<turnstile> \<not> \<not> P \<longleftrightarrow> P"
by fast_prop
(*3*)
-lemma "|- \<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
+lemma "\<turnstile> \<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
by fast_prop
(*4*)
-lemma "|- (\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"
+lemma "\<turnstile> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"
by fast_prop
(*5*)
-lemma "|- ((P \<or> Q) \<longrightarrow> (P \<or> R)) \<longrightarrow> (P \<or> (Q \<longrightarrow> R))"
+lemma "\<turnstile> ((P \<or> Q) \<longrightarrow> (P \<or> R)) \<longrightarrow> (P \<or> (Q \<longrightarrow> R))"
by fast_prop
(*6*)
-lemma "|- P \<or> \<not> P"
+lemma "\<turnstile> P \<or> \<not> P"
by fast_prop
(*7*)
-lemma "|- P \<or> \<not> \<not> \<not> P"
+lemma "\<turnstile> P \<or> \<not> \<not> \<not> P"
by fast_prop
(*8. Peirce's law*)
-lemma "|- ((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
+lemma "\<turnstile> ((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
by fast_prop
(*9*)
-lemma "|- ((P \<or> Q) \<and> (\<not> P \<or> Q) \<and> (P \<or> \<not> Q)) \<longrightarrow> \<not> (\<not> P \<or> \<not> Q)"
+lemma "\<turnstile> ((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 \<longrightarrow> R, R \<longrightarrow> P \<and> Q, P \<longrightarrow> (Q \<or> R) |- P \<longleftrightarrow> Q"
+lemma "Q \<longrightarrow> R, R \<longrightarrow> P \<and> Q, P \<longrightarrow> (Q \<or> R) \<turnstile> P \<longleftrightarrow> Q"
by fast_prop
(*11. Proved in each direction (incorrectly, says Pelletier!!) *)
-lemma "|- P \<longleftrightarrow> P"
+lemma "\<turnstile> P \<longleftrightarrow> P"
by fast_prop
(*12. "Dijkstra's law"*)
-lemma "|- ((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
+lemma "\<turnstile> ((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
by fast_prop
(*13. Distributive law*)
-lemma "|- P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
+lemma "\<turnstile> P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
by fast_prop
(*14*)
-lemma "|- (P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P))"
+lemma "\<turnstile> (P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P))"
by fast_prop
(*15*)
-lemma "|- (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
+lemma "\<turnstile> (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
by fast_prop
(*16*)
-lemma "|- (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"
+lemma "\<turnstile> (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"
by fast_prop
(*17*)
-lemma "|- ((P \<and> (Q \<longrightarrow> R)) \<longrightarrow> S) \<longleftrightarrow> ((\<not> P \<or> Q \<or> S) \<and> (\<not> P \<or> \<not> R \<or> S))"
+lemma "\<turnstile> ((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 20:51:39 2015 +0200
+++ b/src/Sequents/LK/Quantifiers.thy Sat Oct 10 20:54:44 2015 +0200
@@ -9,94 +9,94 @@
imports "../LK"
begin
-lemma "|- (\<forall>x. P) \<longleftrightarrow> P"
+lemma "\<turnstile> (\<forall>x. P) \<longleftrightarrow> P"
by fast
-lemma "|- (\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
+lemma "\<turnstile> (\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
by fast
-lemma "\<forall>u. P(u), \<forall>v. Q(v) |- \<forall>u v. P(u) \<and> Q(v)"
+lemma "\<forall>u. P(u), \<forall>v. Q(v) \<turnstile> \<forall>u v. P(u) \<and> Q(v)"
by fast
text "Permutation of existential quantifier."
-lemma "|- (\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
+lemma "\<turnstile> (\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
by fast
-lemma "|- (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
+lemma "\<turnstile> (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
by fast
(*Converse is invalid*)
-lemma "|- (\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
+lemma "\<turnstile> (\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
by fast
text "Pushing \<forall>into an implication."
-lemma "|- (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
+lemma "\<turnstile> (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
by fast
-lemma "|- (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
+lemma "\<turnstile> (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
by fast
-lemma "|- (\<exists>x. P) \<longleftrightarrow> P"
+lemma "\<turnstile> (\<exists>x. P) \<longleftrightarrow> P"
by fast
text "Distribution of \<exists>over disjunction."
-lemma "|- (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
+lemma "\<turnstile> (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
by fast
(*Converse is invalid*)
-lemma "|- (\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
+lemma "\<turnstile> (\<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 "|- (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
+lemma "\<turnstile> (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
by fast
-lemma "|- (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+lemma "\<turnstile> (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
by fast
-lemma "|- (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
+lemma "\<turnstile> (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
by fast
text "Basic test of quantifier reasoning"
-lemma "|- (\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
+lemma "\<turnstile> (\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
by fast
-lemma "|- (\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
+lemma "\<turnstile> (\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
by fast
text "The following are invalid!"
(*INVALID*)
-lemma "|- (\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
+lemma "\<turnstile> (\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
apply fast?
apply (rule _)
oops
(*INVALID*)
-lemma "|- (\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
+lemma "\<turnstile> (\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
apply fast?
apply (rule _)
oops
(*INVALID*)
-schematic_goal "|- P(?a) \<longrightarrow> (\<forall>x. P(x))"
+schematic_goal "\<turnstile> P(?a) \<longrightarrow> (\<forall>x. P(x))"
apply fast?
apply (rule _)
oops
(*INVALID*)
-schematic_goal "|- (P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))"
+schematic_goal "\<turnstile> (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 "|- (\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
+lemma "\<turnstile> (\<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 \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
+lemma "\<turnstile> (P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
by fast
text "Solving for a Var"
-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)"
+schematic_goal "\<turnstile> (\<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 "|- (\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))"
+lemma "\<turnstile> (\<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 "|- (\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))"
+lemma "\<turnstile> (\<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 "|- (\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))"
+lemma "\<turnstile> (\<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 20:51:39 2015 +0200
+++ b/src/Sequents/LK0.thy Sat Oct 10 20:54:44 2015 +0200
@@ -32,7 +32,7 @@
Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)
syntax
- "_Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
+ "_Trueprop" :: "two_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5)
parse_translation \<open>[(@{syntax_const "_Trueprop"}, K (two_seq_tr @{const_syntax Trueprop}))]\<close>
print_translation \<open>[(@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))]\<close>
@@ -45,34 +45,34 @@
(*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
- contRS: "$H |- $E, $S, $S, $F \<Longrightarrow> $H |- $E, $S, $F" and
- contLS: "$H, $S, $S, $G |- $E \<Longrightarrow> $H, $S, $G |- $E" and
+ contRS: "$H \<turnstile> $E, $S, $S, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and
+ contLS: "$H, $S, $S, $G \<turnstile> $E \<Longrightarrow> $H, $S, $G \<turnstile> $E" and
- thinRS: "$H |- $E, $F \<Longrightarrow> $H |- $E, $S, $F" and
- thinLS: "$H, $G |- $E \<Longrightarrow> $H, $S, $G |- $E" and
+ thinRS: "$H \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and
+ thinLS: "$H, $G \<turnstile> $E \<Longrightarrow> $H, $S, $G \<turnstile> $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
+ exchRS: "$H \<turnstile> $E, $R, $S, $F \<Longrightarrow> $H \<turnstile> $E, $S, $R, $F" and
+ exchLS: "$H, $R, $S, $G \<turnstile> $E \<Longrightarrow> $H, $S, $R, $G \<turnstile> $E" and
- cut: "\<lbrakk>$H |- $E, P; $H, P |- $E\<rbrakk> \<Longrightarrow> $H |- $E" and
+ cut: "\<lbrakk>$H \<turnstile> $E, P; $H, P \<turnstile> $E\<rbrakk> \<Longrightarrow> $H \<turnstile> $E" and
(*Propositional rules*)
- basic: "$H, P, $G |- $E, P, $F" and
+ basic: "$H, P, $G \<turnstile> $E, P, $F" 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
+ conjR: "\<lbrakk>$H\<turnstile> $E, P, $F; $H\<turnstile> $E, Q, $F\<rbrakk> \<Longrightarrow> $H\<turnstile> $E, P \<and> Q, $F" and
+ conjL: "$H, P, Q, $G \<turnstile> $E \<Longrightarrow> $H, P \<and> Q, $G \<turnstile> $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
+ disjR: "$H \<turnstile> $E, P, Q, $F \<Longrightarrow> $H \<turnstile> $E, P \<or> Q, $F" and
+ disjL: "\<lbrakk>$H, P, $G \<turnstile> $E; $H, Q, $G \<turnstile> $E\<rbrakk> \<Longrightarrow> $H, P \<or> Q, $G \<turnstile> $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
+ impR: "$H, P \<turnstile> $E, Q, $F \<Longrightarrow> $H \<turnstile> $E, P \<longrightarrow> Q, $F" and
+ impL: "\<lbrakk>$H,$G \<turnstile> $E,P; $H, Q, $G \<turnstile> $E\<rbrakk> \<Longrightarrow> $H, P \<longrightarrow> Q, $G \<turnstile> $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
+ notR: "$H, P \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, \<not> P, $F" and
+ notL: "$H, $G \<turnstile> $E, P \<Longrightarrow> $H, \<not> P, $G \<turnstile> $E" and
- FalseL: "$H, False, $G |- $E" and
+ FalseL: "$H, False, $G \<turnstile> $E" and
True_def: "True \<equiv> False \<longrightarrow> False" and
iff_def: "P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)"
@@ -80,27 +80,27 @@
axiomatization where
(*Quantifiers*)
- 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
+ allR: "(\<And>x. $H \<turnstile> $E, P(x), $F) \<Longrightarrow> $H \<turnstile> $E, \<forall>x. P(x), $F" and
+ allL: "$H, P(x), $G, \<forall>x. P(x) \<turnstile> $E \<Longrightarrow> $H, \<forall>x. P(x), $G \<turnstile> $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
+ exR: "$H \<turnstile> $E, P(x), $F, \<exists>x. P(x) \<Longrightarrow> $H \<turnstile> $E, \<exists>x. P(x), $F" and
+ exL: "(\<And>x. $H, P(x), $G \<turnstile> $E) \<Longrightarrow> $H, \<exists>x. P(x), $G \<turnstile> $E" and
(*Equality*)
- 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)"
+ refl: "$H \<turnstile> $E, a = a, $F" and
+ subst: "\<And>G H E. $H(a), $G(a) \<turnstile> $E(a) \<Longrightarrow> $H(b), a=b, $G(b) \<turnstile> $E(b)"
(* Reflection *)
axiomatization where
- eq_reflection: "|- x = y \<Longrightarrow> (x \<equiv> y)" and
- iff_reflection: "|- P \<longleftrightarrow> Q \<Longrightarrow> (P \<equiv> Q)"
+ eq_reflection: "\<turnstile> x = y \<Longrightarrow> (x \<equiv> y)" and
+ iff_reflection: "\<turnstile> P \<longleftrightarrow> Q \<Longrightarrow> (P \<equiv> Q)"
(*Descriptions*)
axiomatization where
- 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"
+ The: "\<lbrakk>$H \<turnstile> $E, P(a), $F; \<And>x.$H, P(x) \<turnstile> $E, x=a, $F\<rbrakk> \<Longrightarrow>
+ $H \<turnstile> $E, P(THE x. P(x)), $F"
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)"
@@ -110,26 +110,26 @@
(*contraction*)
-lemma contR: "$H |- $E, P, P, $F \<Longrightarrow> $H |- $E, P, $F"
+lemma contR: "$H \<turnstile> $E, P, P, $F \<Longrightarrow> $H \<turnstile> $E, P, $F"
by (rule contRS)
-lemma contL: "$H, P, P, $G |- $E \<Longrightarrow> $H, P, $G |- $E"
+lemma contL: "$H, P, P, $G \<turnstile> $E \<Longrightarrow> $H, P, $G \<turnstile> $E"
by (rule contLS)
(*thinning*)
-lemma thinR: "$H |- $E, $F \<Longrightarrow> $H |- $E, P, $F"
+lemma thinR: "$H \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, P, $F"
by (rule thinRS)
-lemma thinL: "$H, $G |- $E \<Longrightarrow> $H, P, $G |- $E"
+lemma thinL: "$H, $G \<turnstile> $E \<Longrightarrow> $H, P, $G \<turnstile> $E"
by (rule thinLS)
(*exchange*)
-lemma exchR: "$H |- $E, Q, P, $F \<Longrightarrow> $H |- $E, P, Q, $F"
+lemma exchR: "$H \<turnstile> $E, Q, P, $F \<Longrightarrow> $H \<turnstile> $E, P, Q, $F"
by (rule exchRS)
-lemma exchL: "$H, Q, P, $G |- $E \<Longrightarrow> $H, P, Q, $G |- $E"
+lemma exchL: "$H, Q, P, $G \<turnstile> $E \<Longrightarrow> $H, P, Q, $G \<turnstile> $E"
by (rule exchLS)
ML \<open>
@@ -146,21 +146,21 @@
(** If-and-only-if rules **)
-lemma iffR: "\<lbrakk>$H,P |- $E,Q,$F; $H,Q |- $E,P,$F\<rbrakk> \<Longrightarrow> $H |- $E, P \<longleftrightarrow> Q, $F"
+lemma iffR: "\<lbrakk>$H,P \<turnstile> $E,Q,$F; $H,Q \<turnstile> $E,P,$F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P \<longleftrightarrow> Q, $F"
apply (unfold iff_def)
apply (assumption | rule conjR impR)+
done
-lemma iffL: "\<lbrakk>$H,$G |- $E,P,Q; $H,Q,P,$G |- $E\<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G |- $E"
+lemma iffL: "\<lbrakk>$H,$G \<turnstile> $E,P,Q; $H,Q,P,$G \<turnstile> $E\<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G \<turnstile> $E"
apply (unfold iff_def)
apply (assumption | rule conjL impL basic)+
done
-lemma iff_refl: "$H |- $E, (P \<longleftrightarrow> P), $F"
+lemma iff_refl: "$H \<turnstile> $E, (P \<longleftrightarrow> P), $F"
apply (rule iffR basic)+
done
-lemma TrueR: "$H |- $E, True, $F"
+lemma TrueR: "$H \<turnstile> $E, True, $F"
apply (unfold True_def)
apply (rule impR)
apply (rule basic)
@@ -168,9 +168,9 @@
(*Descriptions*)
lemma the_equality:
- assumes p1: "$H |- $E, P(a), $F"
- and p2: "\<And>x. $H, P(x) |- $E, x=a, $F"
- shows "$H |- $E, (THE x. P(x)) = a, $F"
+ assumes p1: "$H \<turnstile> $E, P(a), $F"
+ and p2: "\<And>x. $H, P(x) \<turnstile> $E, x=a, $F"
+ shows "$H \<turnstile> $E, (THE x. P(x)) = a, $F"
apply (rule cut)
apply (rule_tac [2] p2)
apply (rule The, rule thinR, rule exchRS, rule p1)
@@ -180,12 +180,12 @@
(** Weakened quantifier rules. Incomplete, they let the search terminate.**)
-lemma allL_thin: "$H, P(x), $G |- $E \<Longrightarrow> $H, \<forall>x. P(x), $G |- $E"
+lemma allL_thin: "$H, P(x), $G \<turnstile> $E \<Longrightarrow> $H, \<forall>x. P(x), $G \<turnstile> $E"
apply (rule allL)
apply (erule thinL)
done
-lemma exR_thin: "$H |- $E, P(x), $F \<Longrightarrow> $H |- $E, \<exists>x. P(x), $F"
+lemma exR_thin: "$H \<turnstile> $E, P(x), $F \<Longrightarrow> $H \<turnstile> $E, \<exists>x. P(x), $F"
apply (rule exR)
apply (erule thinR)
done
@@ -233,18 +233,18 @@
lemma mp_R:
- assumes major: "$H |- $E, $F, P \<longrightarrow> Q"
- and minor: "$H |- $E, $F, P"
- shows "$H |- $E, Q, $F"
+ assumes major: "$H \<turnstile> $E, $F, P \<longrightarrow> Q"
+ and minor: "$H \<turnstile> $E, $F, P"
+ shows "$H \<turnstile> $E, Q, $F"
apply (rule thinRS [THEN cut], rule major)
apply step
apply (rule thinR, rule minor)
done
lemma mp_L:
- assumes major: "$H, $G |- $E, P \<longrightarrow> Q"
- and minor: "$H, $G, Q |- $E"
- shows "$H, P, $G |- $E"
+ assumes major: "$H, $G \<turnstile> $E, P \<longrightarrow> Q"
+ and minor: "$H, $G, Q \<turnstile> $E"
+ shows "$H, P, $G \<turnstile> $E"
apply (rule thinL [THEN cut], rule major)
apply step
apply (rule thinL, rule minor)
@@ -254,18 +254,18 @@
(** Two rules to generate left- and right- rules from implications **)
lemma R_of_imp:
- assumes major: "|- P \<longrightarrow> Q"
- and minor: "$H |- $E, $F, P"
- shows "$H |- $E, Q, $F"
+ assumes major: "\<turnstile> P \<longrightarrow> Q"
+ and minor: "$H \<turnstile> $E, $F, P"
+ shows "$H \<turnstile> $E, Q, $F"
apply (rule mp_R)
apply (rule_tac [2] minor)
apply (rule thinRS, rule major [THEN thinLS])
done
lemma L_of_imp:
- assumes major: "|- P \<longrightarrow> Q"
- and minor: "$H, $G, Q |- $E"
- shows "$H, P, $G |- $E"
+ assumes major: "\<turnstile> P \<longrightarrow> Q"
+ and minor: "$H, $G, Q \<turnstile> $E"
+ shows "$H, P, $G \<turnstile> $E"
apply (rule mp_L)
apply (rule_tac [2] minor)
apply (rule thinRS, rule major [THEN thinLS])
@@ -273,24 +273,24 @@
(*Can be used to create implications in a subgoal*)
lemma backwards_impR:
- assumes prem: "$H, $G |- $E, $F, P \<longrightarrow> Q"
- shows "$H, P, $G |- $E, Q, $F"
+ assumes prem: "$H, $G \<turnstile> $E, $F, P \<longrightarrow> Q"
+ shows "$H, P, $G \<turnstile> $E, Q, $F"
apply (rule mp_L)
apply (rule_tac [2] basic)
apply (rule thinR, rule prem)
done
-lemma conjunct1: "|-P \<and> Q \<Longrightarrow> |-P"
+lemma conjunct1: "\<turnstile>P \<and> Q \<Longrightarrow> \<turnstile>P"
apply (erule thinR [THEN cut])
apply fast
done
-lemma conjunct2: "|-P \<and> Q \<Longrightarrow> |-Q"
+lemma conjunct2: "\<turnstile>P \<and> Q \<Longrightarrow> \<turnstile>Q"
apply (erule thinR [THEN cut])
apply fast
done
-lemma spec: "|- (\<forall>x. P(x)) \<Longrightarrow> |- P(x)"
+lemma spec: "\<turnstile> (\<forall>x. P(x)) \<Longrightarrow> \<turnstile> P(x)"
apply (erule thinR [THEN cut])
apply fast
done
@@ -298,10 +298,10 @@
(** Equality **)
-lemma sym: "|- a = b \<longrightarrow> b = a"
+lemma sym: "\<turnstile> a = b \<longrightarrow> b = a"
by (safe add!: subst)
-lemma trans: "|- a = b \<longrightarrow> b = c \<longrightarrow> a = c"
+lemma trans: "\<turnstile> a = b \<longrightarrow> b = c \<longrightarrow> a = c"
by (safe add!: subst)
(* Symmetry of equality in hypotheses *)
@@ -310,18 +310,18 @@
(* Symmetry of equality in hypotheses *)
lemmas symR = sym [THEN R_of_imp]
-lemma transR: "\<lbrakk>$H|- $E, $F, a = b; $H|- $E, $F, b=c\<rbrakk> \<Longrightarrow> $H|- $E, a = c, $F"
+lemma transR: "\<lbrakk>$H\<turnstile> $E, $F, a = b; $H\<turnstile> $E, $F, b=c\<rbrakk> \<Longrightarrow> $H\<turnstile> $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 \<equiv> B) \<Longrightarrow> |- A \<longleftrightarrow> B"
+lemma def_imp_iff: "(A \<equiv> B) \<Longrightarrow> \<turnstile> A \<longleftrightarrow> B"
apply unfold
apply (rule iff_refl)
done
-lemma meta_eq_to_obj_eq: "(A \<equiv> B) \<Longrightarrow> |- A = B"
+lemma meta_eq_to_obj_eq: "(A \<equiv> B) \<Longrightarrow> \<turnstile> A = B"
apply unfold
apply (rule refl)
done
@@ -329,19 +329,19 @@
(** if-then-else rules **)
-lemma if_True: "|- (if True then x else y) = x"
+lemma if_True: "\<turnstile> (if True then x else y) = x"
unfolding If_def by fast
-lemma if_False: "|- (if False then x else y) = y"
+lemma if_False: "\<turnstile> (if False then x else y) = y"
unfolding If_def by fast
-lemma if_P: "|- P \<Longrightarrow> |- (if P then x else y) = x"
+lemma if_P: "\<turnstile> P \<Longrightarrow> \<turnstile> (if P then x else y) = x"
apply (unfold If_def)
apply (erule thinR [THEN cut])
apply fast
done
-lemma if_not_P: "|- \<not> P \<Longrightarrow> |- (if P then x else y) = y"
+lemma if_not_P: "\<turnstile> \<not> P \<Longrightarrow> \<turnstile> (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 20:51:39 2015 +0200
+++ b/src/Sequents/Modal0.thy Sat Oct 10 20:54:44 2015 +0200
@@ -43,12 +43,12 @@
lemmas rewrite_rls = strimp_def streqv_def
-lemma iffR: "\<lbrakk>$H,P |- $E,Q,$F; $H,Q |- $E,P,$F\<rbrakk> \<Longrightarrow> $H |- $E, P \<longleftrightarrow> Q, $F"
+lemma iffR: "\<lbrakk>$H,P \<turnstile> $E,Q,$F; $H,Q \<turnstile> $E,P,$F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P \<longleftrightarrow> Q, $F"
apply (unfold iff_def)
apply (assumption | rule conjR impR)+
done
-lemma iffL: "\<lbrakk>$H,$G |- $E,P,Q; $H,Q,P,$G |- $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G |- $E"
+lemma iffL: "\<lbrakk>$H,$G \<turnstile> $E,P,Q; $H,Q,P,$G \<turnstile> $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G \<turnstile> $E"
apply (unfold iff_def)
apply (assumption | rule conjL impL basic)+
done
--- a/src/Sequents/S4.thy Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/S4.thy Sat Oct 10 20:54:44 2015 +0200
@@ -23,13 +23,13 @@
boxR:
"\<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
+ $E' \<turnstile> $F', P, $G'\<rbrakk> \<Longrightarrow> $E \<turnstile> $F, []P, $G" and
+ boxL: "$E,P,$F,[]P \<turnstile> $G \<Longrightarrow> $E, []P, $F \<turnstile> $G" and
- diaR: "$E |- $F,P,$G,<>P \<Longrightarrow> $E |- $F, <>P, $G" and
+ diaR: "$E \<turnstile> $F,P,$G,<>P \<Longrightarrow> $E \<turnstile> $F, <>P, $G" and
diaL:
"\<lbrakk>$E |L> $E'; $F |L> $F'; $G |R> $G';
- $E', P, $F' |- $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F |- $G"
+ $E', P, $F' \<turnstile> $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F \<turnstile> $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 \<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 "\<turnstile> []P \<longrightarrow> P" by S4_solve
+lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by S4_solve (* normality*)
+lemma "\<turnstile> (P --< Q) \<longrightarrow> []P \<longrightarrow> []Q" by S4_solve
+lemma "\<turnstile> P \<longrightarrow> <>P" 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 "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S4_solve
+lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S4_solve
+lemma "\<turnstile> [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P >-< Q)" by S4_solve
+lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S4_solve
+lemma "\<turnstile> []P \<longleftrightarrow> \<not> <>(\<not> P)" by S4_solve
+lemma "\<turnstile> [](\<not> P) \<longleftrightarrow> \<not> <>P" by S4_solve
+lemma "\<turnstile> \<not> []P \<longleftrightarrow> <>(\<not> P)" by S4_solve
+lemma "\<turnstile> [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by S4_solve
+lemma "\<turnstile> \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>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
+lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S4_solve
+lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S4_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S4_solve
+lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S4_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S4_solve
+lemma "\<turnstile> <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by S4_solve
+lemma "\<turnstile> (P --< Q) \<and> (Q --< R) \<longrightarrow> (P --< R)" by S4_solve
+lemma "\<turnstile> []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by S4_solve
(* Theorems of system S4 from Hughes and Cresswell, p.46 *)
-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
+lemma "\<turnstile> []A \<longrightarrow> A" by S4_solve (* refexivity *)
+lemma "\<turnstile> []A \<longrightarrow> [][]A" by S4_solve (* transitivity *)
+lemma "\<turnstile> []A \<longrightarrow> <>A" by S4_solve (* seriality *)
+lemma "\<turnstile> <>[](<>A \<longrightarrow> []<>A)" by S4_solve
+lemma "\<turnstile> <>[](<>[]A \<longrightarrow> []A)" by S4_solve
+lemma "\<turnstile> []P \<longleftrightarrow> [][]P" by S4_solve
+lemma "\<turnstile> <>P \<longleftrightarrow> <><>P" by S4_solve
+lemma "\<turnstile> <>[]<>P \<longrightarrow> <>P" by S4_solve
+lemma "\<turnstile> []<>P \<longleftrightarrow> []<>[]<>P" by S4_solve
+lemma "\<turnstile> <>[]P \<longleftrightarrow> <>[]<>[]P" by S4_solve
(* Theorems for system S4 from Hughes and Cresswell, p.60 *)
-lemma "|- []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S4_solve
-lemma "|- ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S4_solve
+lemma "\<turnstile> []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S4_solve
+lemma "\<turnstile> ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S4_solve
(* These are from Hailpern, LNCS 129 *)
-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 "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S4_solve
+lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S4_solve
+lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" 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 "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> (<>P \<longrightarrow> <>Q)" by S4_solve
+lemma "\<turnstile> []P \<longrightarrow> []<>P" by S4_solve
+lemma "\<turnstile> <>[]P \<longrightarrow> <>P" 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 "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S4_solve
+lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S4_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S4_solve
+lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S4_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S4_solve
end
--- a/src/Sequents/S43.thy Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/S43.thy Sat Oct 10 20:54:44 2015 +0200
@@ -48,32 +48,32 @@
(* ie *)
(* S1...Sk,Sk+1...Sk+m *)
(* ---------------------------------- *)
-(* <>P1...<>Pk, $G |- $H, []Q1...[]Qm *)
+(* <>P1...<>Pk, $G \<turnstile> $H, []Q1...[]Qm *)
(* *)
-(* where Si == <>P1...<>Pi-1,<>Pi+1,..<>Pk,Pi, $G * |- $H *, []Q1...[]Qm *)
-(* and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj *)
+(* where Si == <>P1...<>Pi-1,<>Pi+1,..<>Pk,Pi, $G * \<turnstile> $H *, []Q1...[]Qm *)
+(* and Sj == <>P1...<>Pk, $G * \<turnstile> $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj *)
(* and 1<=i<=k and k<j<=k+m *)
S43pi0: "S43pi $L;; $R;; $Lbox; $Rdia" and
S43pi1:
- "\<lbrakk>(S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox |- $R,$Rdia\<rbrakk> \<Longrightarrow>
+ "\<lbrakk>(S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox \<turnstile> $R,$Rdia\<rbrakk> \<Longrightarrow>
S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia" and
S43pi2:
- "\<lbrakk>(S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox |- $R',P,$R,$Rdia\<rbrakk> \<Longrightarrow>
+ "\<lbrakk>(S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox \<turnstile> $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 \<Longrightarrow> $E, []P, $F |- $G" and
- diaR: "$E |- $F, P, $G, <>P \<Longrightarrow> $E |- $F, <>P, $G" and
+ boxL: "$E, P, $F, []P \<turnstile> $G \<Longrightarrow> $E, []P, $F \<turnstile> $G" and
+ diaR: "$E \<turnstile> $F, P, $G, <>P \<Longrightarrow> $E \<turnstile> $F, <>P, $G" and
pi1:
"\<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
+ $L1, <>P, $L2 \<turnstile> $R" and
pi2:
"\<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"
+ $L \<turnstile> $R1, []P, $R2"
ML \<open>
@@ -97,108 +97,108 @@
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
-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 "\<turnstile> []P \<longrightarrow> P" by S43_solve
+lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by S43_solve (* normality*)
+lemma "\<turnstile> (P--<Q) \<longrightarrow> []P \<longrightarrow> []Q" by S43_solve
+lemma "\<turnstile> P \<longrightarrow> <>P" 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 "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
+lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
+lemma "\<turnstile> [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P>-<Q)" by S43_solve
+lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S43_solve
+lemma "\<turnstile> []P \<longleftrightarrow> \<not> <>(\<not> P)" by S43_solve
+lemma "\<turnstile> [](\<not>P) \<longleftrightarrow> \<not> <>P" by S43_solve
+lemma "\<turnstile> \<not> []P \<longleftrightarrow> <>(\<not> P)" by S43_solve
+lemma "\<turnstile> [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by S43_solve
+lemma "\<turnstile> \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>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
+lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
+lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
+lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
+lemma "\<turnstile> <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by S43_solve
+lemma "\<turnstile> (P --< Q) \<and> (Q --<R ) \<longrightarrow> (P --< R)" by S43_solve
+lemma "\<turnstile> []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
(* Theorems of system S4 from Hughes and Cresswell, p.46 *)
-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
+lemma "\<turnstile> []A \<longrightarrow> A" by S43_solve (* refexivity *)
+lemma "\<turnstile> []A \<longrightarrow> [][]A" by S43_solve (* transitivity *)
+lemma "\<turnstile> []A \<longrightarrow> <>A" by S43_solve (* seriality *)
+lemma "\<turnstile> <>[](<>A \<longrightarrow> []<>A)" by S43_solve
+lemma "\<turnstile> <>[](<>[]A \<longrightarrow> []A)" by S43_solve
+lemma "\<turnstile> []P \<longleftrightarrow> [][]P" by S43_solve
+lemma "\<turnstile> <>P \<longleftrightarrow> <><>P" by S43_solve
+lemma "\<turnstile> <>[]<>P \<longrightarrow> <>P" by S43_solve
+lemma "\<turnstile> []<>P \<longleftrightarrow> []<>[]<>P" by S43_solve
+lemma "\<turnstile> <>[]P \<longleftrightarrow> <>[]<>[]P" by S43_solve
(* Theorems for system S4 from Hughes and Cresswell, p.60 *)
-lemma "|- []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S43_solve
-lemma "|- ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S43_solve
+lemma "\<turnstile> []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S43_solve
+lemma "\<turnstile> ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S43_solve
(* These are from Hailpern, LNCS 129 *)
-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 "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
+lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
+lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" 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 "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> (<>P \<longrightarrow> <>Q)" by S43_solve
+lemma "\<turnstile> []P \<longrightarrow> []<>P" by S43_solve
+lemma "\<turnstile> <>[]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 \<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 "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
+lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
+lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
(* Theorems of system S43 *)
-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
+lemma "\<turnstile> <>[]P \<longrightarrow> []<>P" by S43_solve
+lemma "\<turnstile> <>[]P \<longrightarrow> [][]<>P" by S43_solve
+lemma "\<turnstile> [](<>P \<or> <>Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve
+lemma "\<turnstile> <>[]P \<and> <>[]Q \<longrightarrow> <>([]P \<and> []Q)" by S43_solve
+lemma "\<turnstile> []([]P \<longrightarrow> []Q) \<or> []([]Q \<longrightarrow> []P)" by S43_solve
+lemma "\<turnstile> [](<>P \<longrightarrow> <>Q) \<or> [](<>Q \<longrightarrow> <>P)" by S43_solve
+lemma "\<turnstile> []([]P \<longrightarrow> Q) \<or> []([]Q \<longrightarrow> P)" by S43_solve
+lemma "\<turnstile> [](P \<longrightarrow> <>Q) \<or> [](Q \<longrightarrow> <>P)" by S43_solve
+lemma "\<turnstile> [](P \<longrightarrow> []Q \<longrightarrow> R) \<or> [](P \<or> ([]R \<longrightarrow> Q))" by S43_solve
+lemma "\<turnstile> [](P \<or> (Q \<longrightarrow> <>C)) \<or> [](P \<longrightarrow> C \<longrightarrow> <>Q)" by S43_solve
+lemma "\<turnstile> []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve
+lemma "\<turnstile> <>P \<and> <>Q \<longrightarrow> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<and> []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve
+lemma "\<turnstile> <>P \<and> <>Q \<longrightarrow> <>(P \<and> Q) \<or> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve
+lemma "\<turnstile> <>[]<>P \<longleftrightarrow> []<>P" by S43_solve
+lemma "\<turnstile> []<>[]P \<longleftrightarrow> <>[]P" by S43_solve
(* These are from Hailpern, LNCS 129 *)
-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 "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
+lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
+lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> []P \<longrightarrow> <>Q" 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 "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> <>P \<longrightarrow> <>Q" by S43_solve
+lemma "\<turnstile> []P \<longrightarrow> []<>P" by S43_solve
+lemma "\<turnstile> <>[]P \<longrightarrow> <>P" by S43_solve
+lemma "\<turnstile> []<>[]P \<longrightarrow> []<>P" by S43_solve
+lemma "\<turnstile> <>[]P \<longrightarrow> <>[]<>P" by S43_solve
+lemma "\<turnstile> <>[]P \<longrightarrow> []<>P" by S43_solve
+lemma "\<turnstile> []<>[]P \<longleftrightarrow> <>[]P" by S43_solve
+lemma "\<turnstile> <>[]<>P \<longleftrightarrow> []<>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 \<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
+lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
+lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
+lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve
+lemma "\<turnstile> <>[]P \<and> <>[]Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "\<turnstile> <>[](P \<and> Q) \<longleftrightarrow> <>[]P \<and> <>[]Q" by S43_solve
+lemma "\<turnstile> []<>(P \<or> Q) \<longleftrightarrow> []<>P \<or> []<>Q" by S43_solve
end
--- a/src/Sequents/Sequents.thy Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/Sequents.thy Sat Oct 10 20:54:44 2015 +0200
@@ -21,8 +21,8 @@
typedecl seq'
consts
- SeqO' :: "[o,seq']=>seq'"
- Seq1' :: "o=>seq'"
+ SeqO' :: "[o,seq']\<Rightarrow>seq'"
+ Seq1' :: "o\<Rightarrow>seq'"
subsection \<open>Concrete syntax\<close>
@@ -31,28 +31,28 @@
syntax
"_SeqEmp" :: seq ("")
- "_SeqApp" :: "[seqobj,seqcont] => seq" ("__")
+ "_SeqApp" :: "[seqobj,seqcont] \<Rightarrow> seq" ("__")
"_SeqContEmp" :: seqcont ("")
- "_SeqContApp" :: "[seqobj,seqcont] => seqcont" (",/ __")
+ "_SeqContApp" :: "[seqobj,seqcont] \<Rightarrow> seqcont" (",/ __")
- "_SeqO" :: "o => seqobj" ("_")
- "_SeqId" :: "'a => seqobj" ("$_")
+ "_SeqO" :: "o \<Rightarrow> seqobj" ("_")
+ "_SeqId" :: "'a \<Rightarrow> seqobj" ("$_")
-type_synonym single_seqe = "[seq,seqobj] => prop"
-type_synonym single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
-type_synonym two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
-type_synonym two_seqe = "[seq, seq] => prop"
-type_synonym three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
-type_synonym three_seqe = "[seq, seq, seq] => prop"
-type_synonym four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
-type_synonym four_seqe = "[seq, seq, seq, seq] => prop"
-type_synonym sequence_name = "seq'=>seq'"
+type_synonym single_seqe = "[seq,seqobj] \<Rightarrow> prop"
+type_synonym single_seqi = "[seq'\<Rightarrow>seq',seq'\<Rightarrow>seq'] \<Rightarrow> prop"
+type_synonym two_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
+type_synonym two_seqe = "[seq, seq] \<Rightarrow> prop"
+type_synonym three_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
+type_synonym three_seqe = "[seq, seq, seq] \<Rightarrow> prop"
+type_synonym four_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
+type_synonym four_seqe = "[seq, seq, seq, seq] \<Rightarrow> prop"
+type_synonym sequence_name = "seq'\<Rightarrow>seq'"
syntax
(*Constant to allow definitions of SEQUENCES of formulas*)
- "_Side" :: "seq=>(seq'=>seq')" ("<<(_)>>")
+ "_Side" :: "seq\<Rightarrow>(seq'\<Rightarrow>seq')" ("<<(_)>>")
ML \<open>
--- a/src/Sequents/T.thy Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/T.thy Sat Oct 10 20:54:44 2015 +0200
@@ -23,12 +23,12 @@
boxR:
"\<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
+ $E' \<turnstile> $F', P, $G'\<rbrakk> \<Longrightarrow> $E \<turnstile> $F, []P, $G" and
+ boxL: "$E, P, $F \<turnstile> $G \<Longrightarrow> $E, []P, $F \<turnstile> $G" and
+ diaR: "$E \<turnstile> $F, P, $G \<Longrightarrow> $E \<turnstile> $F, <>P, $G" and
diaL:
"\<lbrakk>$E |L> $E'; $F |L> $F'; $G |R> $G';
- $E', P, $F'|- $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F |- $G"
+ $E', P, $F'\<turnstile> $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F \<turnstile> $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 \<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 "\<turnstile> []P \<longrightarrow> P" by T_solve
+lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by T_solve (* normality*)
+lemma "\<turnstile> (P --< Q) \<longrightarrow> []P \<longrightarrow> []Q" by T_solve
+lemma "\<turnstile> P \<longrightarrow> <>P" 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 "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by T_solve
+lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by T_solve
+lemma "\<turnstile> [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P >-< Q)" by T_solve
+lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by T_solve
+lemma "\<turnstile> []P \<longleftrightarrow> \<not> <>(\<not> P)" by T_solve
+lemma "\<turnstile> [](\<not> P) \<longleftrightarrow> \<not> <>P" by T_solve
+lemma "\<turnstile> \<not> []P \<longleftrightarrow> <>(\<not> P)" by T_solve
+lemma "\<turnstile> [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by T_solve
+lemma "\<turnstile> \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>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
+lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by T_solve
+lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by T_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by T_solve
+lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by T_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by T_solve
+lemma "\<turnstile> <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by T_solve
+lemma "\<turnstile> (P --< Q) \<and> (Q --< R ) \<longrightarrow> (P --< R)" by T_solve
+lemma "\<turnstile> []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by T_solve
end
--- a/src/Sequents/Washing.thy Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/Washing.thy Sat Oct 10 20:54:44 2015 +0200
@@ -15,19 +15,19 @@
clean :: o
where
change:
- "dollar |- (quarter >< quarter >< quarter >< quarter)" and
+ "dollar \<turnstile> (quarter >< quarter >< quarter >< quarter)" and
load1:
- "quarter , quarter , quarter , quarter , quarter |- loaded" and
+ "quarter , quarter , quarter , quarter , quarter \<turnstile> loaded" and
load2:
- "dollar , quarter |- loaded" and
+ "dollar , quarter \<turnstile> loaded" and
wash:
- "loaded , dirty |- wet" and
+ "loaded , dirty \<turnstile> wet" and
dry:
- "wet, quarter , quarter , quarter |- clean"
+ "wet, quarter , quarter , quarter \<turnstile> clean"
(* "activate" definitions for use in proof *)
@@ -39,17 +39,17 @@
(* a load of dirty clothes and two dollars gives you clean clothes *)
-lemma "dollar , dollar , dirty |- clean"
+lemma "dollar , dollar , dirty \<turnstile> clean"
by (best add!: changeI load1I washI dryI)
(* order of premises doesn't matter *)
-lemma "dollar , dirty , dollar |- clean"
+lemma "dollar , dirty , dollar \<turnstile> clean"
by (best add!: changeI load1I washI dryI)
(* alternative formulation *)
-lemma "dollar , dollar |- dirty -o clean"
+lemma "dollar , dollar \<turnstile> dirty -o clean"
by (best add!: changeI load1I washI dryI)
end