(* Title: Sequents/ILL.thy
Author: Sara Kalvala and Valeria de Paiva
Copyright 1995 University of Cambridge
*)
theory ILL
imports Sequents
begin
consts
Trueprop :: "two_seqi"
tens :: "[o, o] \<Rightarrow> o" (infixr "><" 35)
limp :: "[o, o] \<Rightarrow> o" (infixr "-o" 45)
FShriek :: "o \<Rightarrow> o" ("! _" [100] 1000)
lconj :: "[o, o] \<Rightarrow> o" (infixr "&&" 35)
ldisj :: "[o, o] \<Rightarrow> o" (infixr "++" 35)
zero :: "o" ("0")
top :: "o" ("1")
eye :: "o" ("I")
(* context manipulation *)
Context :: "two_seqi"
(* promotion rule *)
PromAux :: "three_seqi"
syntax
"_Trueprop" :: "single_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5)
"_Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5)
"_PromAux" :: "three_seqe" ("promaux {_||_||_}")
parse_translation \<open>
[(\<^syntax_const>\<open>_Trueprop\<close>, K (single_tr \<^const_syntax>\<open>Trueprop\<close>)),
(\<^syntax_const>\<open>_Context\<close>, K (two_seq_tr \<^const_syntax>\<open>Context\<close>)),
(\<^syntax_const>\<open>_PromAux\<close>, K (three_seq_tr \<^const_syntax>\<open>PromAux\<close>))]
\<close>
print_translation \<open>
[(\<^const_syntax>\<open>Trueprop\<close>, K (single_tr' \<^syntax_const>\<open>_Trueprop\<close>)),
(\<^const_syntax>\<open>Context\<close>, K (two_seq_tr' \<^syntax_const>\<open>_Context\<close>)),
(\<^const_syntax>\<open>PromAux\<close>, K (three_seq_tr' \<^syntax_const>\<open>_PromAux\<close>))]
\<close>
definition liff :: "[o, o] \<Rightarrow> o" (infixr "o-o" 45)
where "P o-o Q == (P -o Q) >< (Q -o P)"
definition aneg :: "o\<Rightarrow>o" ("~_")
where "~A == A -o 0"
axiomatization where
identity: "P \<turnstile> P" and
zerol: "$G, 0, $H \<turnstile> A" and
(* RULES THAT DO NOT DIVIDE CONTEXT *)
derelict: "$F, A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and
(* unfortunately, this one removes !A *)
contract: "$F, !A, !A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> 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 \<turnstile> !B" and
promote1: "promaux{!A, $G || $H || B}
\<Longrightarrow> promaux {$G || $H, !A || B}" and
promote0: "$G \<turnstile> A \<Longrightarrow> promaux {$G || || A}" and
tensl: "$H, A, B, $G \<turnstile> C \<Longrightarrow> $H, A >< B, $G \<turnstile> C" and
impr: "A, $F \<turnstile> B \<Longrightarrow> $F \<turnstile> A -o B" and
conjr: "\<lbrakk>$F \<turnstile> A ;
$F \<turnstile> B\<rbrakk>
\<Longrightarrow> $F \<turnstile> (A && B)" and
conjll: "$G, A, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and
conjlr: "$G, B, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> 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 \<turnstile> A ;
$J \<turnstile> B\<rbrakk>
\<Longrightarrow> $G \<turnstile> A >< B" and
impl: "\<lbrakk>$G, $F :=: $J, $H ;
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 \<turnstile> A ;
$J1, $J2, A, $J3, $J4 \<turnstile> B\<rbrakk> \<Longrightarrow> $F \<turnstile> B" and
(* CONTEXT RULES *)
context1: "$G :=: $G" and
context2: "$F, $G :=: $H, !A, $G \<Longrightarrow> $F, A, $G :=: $H, !A, $G" and
context3: "$F, $G :=: $H, $J \<Longrightarrow> $F, A, $G :=: $H, A, $J" and
context4a: "$F :=: $H, $G \<Longrightarrow> $F :=: $H, !A, $G" and
context4b: "$F, $H :=: $G \<Longrightarrow> $F, !A, $H :=: $G" and
context5: "$F, $G :=: $H \<Longrightarrow> $G, $F :=: $H"
text "declarations for lazy classical reasoning:"
lemmas [safe] =
context3
context2
promote0
disjl
conjr
tensl
lemmas [unsafe] =
context4b
context4a
context1
promote2
promote1
weaken
derelict
impl
tensr
impr
disjrr
disjrl
conjlr
conjll
zerol
identity
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)
apply (rule context1)
apply assumption
done
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) \<turnstile> !A")
apply assumption
apply best
prefer 3
apply (subgoal_tac "! (A && B) \<turnstile> !B")
apply assumption
apply best
apply (rule_tac [2] context1)
apply (rule_tac [2] tensl)
prefer 2 apply assumption
apply (rule context3)
apply (rule context3)
apply (rule context1)
done
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 \<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 \<turnstile> A"
apply (rule impl)
apply (rule_tac [3] identity)
apply (rule context3)
apply (rule context1)
apply (rule zerol)
done
lemma contrad2: "$F, !B, $G, (!B) -o 0, $H \<turnstile> A"
apply (rule impl)
apply (rule_tac [3] identity)
apply (rule context3)
apply (rule context1)
apply (rule zerol)
done
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 \<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)
apply (rule context3)
apply (rule context3)
apply (rule context1)
done
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)
apply (rule context3)
apply (rule context3)
apply (rule context1)
done
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 \<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)
apply (rule context3)
apply (rule context1)
done
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) \<turnstile> (!((!A) -o B)) -o 0"
by best
lemma a_not_a: "!A -o (!A -o 0) \<turnstile> !A -o 0"
apply (rule impr)
apply (rule contract)
apply (rule impl)
apply (rule_tac [3] identity)
apply (rule context1)
apply best
done
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
apply best
done
ML \<open>
val safe_pack =
\<^context>
|> fold_rev Cla.add_safe @{thms conj_lemma ll_mp contrad1
contrad2 mp_rule1 mp_rule2 o_a_rule a_not_a_rule}
|> Cla.add_unsafe @{thm aux_impl}
|> Cla.get_pack;
val power_pack =
Cla.put_pack safe_pack \<^context>
|> Cla.add_unsafe @{thm impr_contr_der}
|> Cla.get_pack;
\<close>
method_setup best_safe =
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack safe_pack ctxt)))\<close>
method_setup best_power =
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack power_pack ctxt)))\<close>
(* Some examples from Troelstra and van Dalen *)
lemma "!((!A) -o ((!B) -o 0)) \<turnstile> (!(A && B)) -o 0"
by best_safe
lemma "!((!(A && B)) -o 0) \<turnstile> !((!A) -o ((!B) -o 0))"
by best_safe
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) ) \<turnstile>
(!((! ((!A) -o B) ) -o 0)) -o 0"
by best_power
end