(* Title: LK/LK0.thy ID: $Id: LK0.thy,v 1.10 2005/09/18 13:20:08 wenzelm Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge There may be printing problems if a seqent is in expanded normal form (eta-expanded, beta-contracted) *) header {* Classical First-Order Sequent Calculus *} theory LK0 imports Sequents begin global classes "term" defaultsort "term" consts Trueprop :: "two_seqi" True :: o False :: o "=" :: "['a,'a] => o" (infixl 50) Not :: "o => o" ("~ _" [40] 40) "&" :: "[o,o] => o" (infixr 35) "|" :: "[o,o] => o" (infixr 30) "-->" :: "[o,o] => o" (infixr 25) "<->" :: "[o,o] => o" (infixr 25) The :: "('a => o) => 'a" (binder "THE " 10) All :: "('a => o) => o" (binder "ALL " 10) Ex :: "('a => o) => o" (binder "EX " 10) syntax "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5) "_not_equal" :: "['a, 'a] => o" (infixl "~=" 50) parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *} print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *} translations "x ~= y" == "~ (x = y)" syntax (xsymbols) Not :: "o => o" ("¬ _" [40] 40) "op &" :: "[o, o] => o" (infixr "∧" 35) "op |" :: "[o, o] => o" (infixr "∨" 30) "op -->" :: "[o, o] => o" (infixr "-->" 25) "op <->" :: "[o, o] => o" (infixr "<->" 25) "ALL " :: "[idts, o] => o" ("(3∀_./ _)" [0, 10] 10) "EX " :: "[idts, o] => o" ("(3∃_./ _)" [0, 10] 10) "EX! " :: "[idts, o] => o" ("(3∃!_./ _)" [0, 10] 10) "_not_equal" :: "['a, 'a] => o" (infixl "≠" 50) syntax (HTML output) Not :: "o => o" ("¬ _" [40] 40) "op &" :: "[o, o] => o" (infixr "∧" 35) "op |" :: "[o, o] => o" (infixr "∨" 30) "ALL " :: "[idts, o] => o" ("(3∀_./ _)" [0, 10] 10) "EX " :: "[idts, o] => o" ("(3∃_./ _)" [0, 10] 10) "EX! " :: "[idts, o] => o" ("(3∃!_./ _)" [0, 10] 10) "_not_equal" :: "['a, 'a] => o" (infixl "≠" 50) local axioms (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *) contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F" contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E" thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F" thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E" exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F" exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E" cut: "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E" (*Propositional rules*) basic: "$H, P, $G |- $E, P, $F" conjR: "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" disjR: "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" disjL: "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" impR: "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" impL: "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" notR: "$H, P |- $E, $F ==> $H |- $E, ~P, $F" notL: "$H, $G |- $E, P ==> $H, ~P, $G |- $E" FalseL: "$H, False, $G |- $E" True_def: "True == False-->False" iff_def: "P<->Q == (P-->Q) & (Q-->P)" (*Quantifiers*) allR: "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F" allL: "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E" exR: "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F" exL: "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E" (*Equality*) refl: "$H |- $E, a=a, $F" subst: "$H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)" (* Reflection *) eq_reflection: "|- x=y ==> (x==y)" iff_reflection: "|- P<->Q ==> (P==Q)" (*Descriptions*) The: "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> $H |- $E, P(THE x. P(x)), $F" constdefs If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)" setup prover_setup ML {* use_legacy_bindings (the_context ()) *} end
theorem contR:
$H |- $E, P, P, $F ==> $H |- $E, P, $F
theorem contL:
$H, P, P, $G |- $E ==> $H, P, $G |- $E
theorem thinR:
$H |- $E, $F ==> $H |- $E, P, $F
theorem thinL:
$H, $G |- $E ==> $H, P, $G |- $E
theorem exchR:
$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F
theorem exchL:
$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E
theorem iffR:
[| $H, P |- $E, Q, $F; $H, Q |- $E, P, $F |] ==> $H |- $E, P <-> Q, $F
theorem iffL:
[| $H, $G |- $E, P, Q; $H, Q, P, $G |- $E |] ==> $H, P <-> Q, $G |- $E
theorem iff_refl:
$H |- $E, P <-> P, $F
theorem TrueR:
$H |- $E, True, $F
theorem the_equality:
[| $H |- $E, P(a), $F; !!x. $H, P(x) |- $E, x = a, $F |] ==> $H |- $E, (THE x. P(x)) = a, $F
theorem allL_thin:
$H, P(x), $G |- $E ==> $H, ∀x. P(x), $G |- $E
theorem exR_thin:
$H |- $E, P(x), $F ==> $H |- $E, ∃x. P(x), $F
theorem mp_R:
[| $H |- $E, $F, P --> Q; $H |- $E, $F, P |] ==> $H |- $E, Q, $F
theorem mp_L:
[| $H, $G |- $E, P --> Q; $H, $G, Q |- $E |] ==> $H, P, $G |- $E
theorem R_of_imp:
[| |- P --> Q; $H |- $E, $F, P |] ==> $H |- $E, Q, $F
theorem L_of_imp:
[| |- P --> Q; $H, $G, Q |- $E |] ==> $H, P, $G |- $E
theorem backwards_impR:
$H, $G |- $E, $F, P --> Q ==> $H, P, $G |- $E, Q, $F
theorem conjunct1:
|- P ∧ Q ==> |- P
theorem conjunct2:
|- P ∧ Q ==> |- Q
theorem spec:
|- ∀x. P(x) ==> |- P(x)
theorem sym:
|- a = b --> b = a
theorem trans:
|- a = b --> b = c --> a = c
theorem symL:
$H, $G, b = a |- $E ==> $H, a = b, $G |- $E
theorem symR:
$H |- $E, $F, a = b ==> $H |- $E, b = a, $F
theorem transR:
[| $H |- $E, $F, a = b; $H |- $E, $F, b = c |] ==> $H |- $E, a = c, $F
theorem def_imp_iff:
A == B ==> |- A <-> B
theorem meta_eq_to_obj_eq:
A == B ==> |- A = B