src/Sequents/LK.thy
author wenzelm
Mon Mar 19 21:10:33 2012 +0100 (2012-03-19)
changeset 47022 8eac39af4ec0
parent 45602 2a858377c3d2
child 48891 c0eafbd55de3
permissions -rw-r--r--
moved some legacy stuff;
     1 (*  Title:      Sequents/LK.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     5 Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
     6 link between |- and ==>, needed for instance to prove imp_cong.
     7 
     8 Axiom left_cong allows the simplifier to use left-side formulas.  Ideally it
     9 should be derived from lower-level axioms.
    10 
    11 CANNOT be added to LK0.thy because modal logic is built upon it, and
    12 various modal rules would become inconsistent.
    13 *)
    14 
    15 theory LK
    16 imports LK0
    17 uses ("simpdata.ML")
    18 begin
    19 
    20 axiomatization where
    21   monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q" and
    22 
    23   left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
    24                ==> (P, $H |- $F) == (P', $H' |- $F')"
    25 
    26 
    27 subsection {* Rewrite rules *}
    28 
    29 lemma conj_simps:
    30   "|- P & True <-> P"
    31   "|- True & P <-> P"
    32   "|- P & False <-> False"
    33   "|- False & P <-> False"
    34   "|- P & P <-> P"
    35   "|- P & P & Q <-> P & Q"
    36   "|- P & ~P <-> False"
    37   "|- ~P & P <-> False"
    38   "|- (P & Q) & R <-> P & (Q & R)"
    39   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    40   done
    41 
    42 lemma disj_simps:
    43   "|- P | True <-> True"
    44   "|- True | P <-> True"
    45   "|- P | False <-> P"
    46   "|- False | P <-> P"
    47   "|- P | P <-> P"
    48   "|- P | P | Q <-> P | Q"
    49   "|- (P | Q) | R <-> P | (Q | R)"
    50   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    51   done
    52 
    53 lemma not_simps:
    54   "|- ~ False <-> True"
    55   "|- ~ True <-> False"
    56   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    57   done
    58 
    59 lemma imp_simps:
    60   "|- (P --> False) <-> ~P"
    61   "|- (P --> True) <-> True"
    62   "|- (False --> P) <-> True"
    63   "|- (True --> P) <-> P"
    64   "|- (P --> P) <-> True"
    65   "|- (P --> ~P) <-> ~P"
    66   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    67   done
    68 
    69 lemma iff_simps:
    70   "|- (True <-> P) <-> P"
    71   "|- (P <-> True) <-> P"
    72   "|- (P <-> P) <-> True"
    73   "|- (False <-> P) <-> ~P"
    74   "|- (P <-> False) <-> ~P"
    75   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    76   done
    77 
    78 lemma quant_simps:
    79   "!!P. |- (ALL x. P) <-> P"
    80   "!!P. |- (ALL x. x=t --> P(x)) <-> P(t)"
    81   "!!P. |- (ALL x. t=x --> P(x)) <-> P(t)"
    82   "!!P. |- (EX x. P) <-> P"
    83   "!!P. |- (EX x. x=t & P(x)) <-> P(t)"
    84   "!!P. |- (EX x. t=x & P(x)) <-> P(t)"
    85   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
    86   done
    87 
    88 
    89 subsection {* Miniscoping: pushing quantifiers in *}
    90 
    91 text {*
    92   We do NOT distribute of ALL over &, or dually that of EX over |
    93   Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
    94   show that this step can increase proof length!
    95 *}
    96 
    97 text {*existential miniscoping*}
    98 lemma ex_simps:
    99   "!!P Q. |- (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
   100   "!!P Q. |- (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
   101   "!!P Q. |- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
   102   "!!P Q. |- (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
   103   "!!P Q. |- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q"
   104   "!!P Q. |- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"
   105   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
   106   done
   107 
   108 text {*universal miniscoping*}
   109 lemma all_simps:
   110   "!!P Q. |- (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
   111   "!!P Q. |- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
   112   "!!P Q. |- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q"
   113   "!!P Q. |- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"
   114   "!!P Q. |- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
   115   "!!P Q. |- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
   116   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
   117   done
   118 
   119 text {*These are NOT supplied by default!*}
   120 lemma distrib_simps:
   121   "|- P & (Q | R) <-> P&Q | P&R"
   122   "|- (Q | R) & P <-> Q&P | R&P"
   123   "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"
   124   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
   125   done
   126 
   127 lemma P_iff_F: "|- ~P ==> |- (P <-> False)"
   128   apply (erule thinR [THEN cut])
   129   apply (tactic {* fast_tac LK_pack 1 *})
   130   done
   131 
   132 lemmas iff_reflection_F = P_iff_F [THEN iff_reflection]
   133 
   134 lemma P_iff_T: "|- P ==> |- (P <-> True)"
   135   apply (erule thinR [THEN cut])
   136   apply (tactic {* fast_tac LK_pack 1 *})
   137   done
   138 
   139 lemmas iff_reflection_T = P_iff_T [THEN iff_reflection]
   140 
   141 
   142 lemma LK_extra_simps:
   143   "|- P | ~P"
   144   "|- ~P | P"
   145   "|- ~ ~ P <-> P"
   146   "|- (~P --> P) <-> P"
   147   "|- (~P <-> ~Q) <-> (P<->Q)"
   148   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
   149   done
   150 
   151 
   152 subsection {* Named rewrite rules *}
   153 
   154 lemma conj_commute: "|- P&Q <-> Q&P"
   155   and conj_left_commute: "|- P&(Q&R) <-> Q&(P&R)"
   156   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
   157   done
   158 
   159 lemmas conj_comms = conj_commute conj_left_commute
   160 
   161 lemma disj_commute: "|- P|Q <-> Q|P"
   162   and disj_left_commute: "|- P|(Q|R) <-> Q|(P|R)"
   163   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
   164   done
   165 
   166 lemmas disj_comms = disj_commute disj_left_commute
   167 
   168 lemma conj_disj_distribL: "|- P&(Q|R) <-> (P&Q | P&R)"
   169   and conj_disj_distribR: "|- (P|Q)&R <-> (P&R | Q&R)"
   170 
   171   and disj_conj_distribL: "|- P|(Q&R) <-> (P|Q) & (P|R)"
   172   and disj_conj_distribR: "|- (P&Q)|R <-> (P|R) & (Q|R)"
   173 
   174   and imp_conj_distrib: "|- (P --> (Q&R)) <-> (P-->Q) & (P-->R)"
   175   and imp_conj: "|- ((P&Q)-->R)   <-> (P --> (Q --> R))"
   176   and imp_disj: "|- (P|Q --> R)   <-> (P-->R) & (Q-->R)"
   177 
   178   and imp_disj1: "|- (P-->Q) | R <-> (P-->Q | R)"
   179   and imp_disj2: "|- Q | (P-->R) <-> (P-->Q | R)"
   180 
   181   and de_Morgan_disj: "|- (~(P | Q)) <-> (~P & ~Q)"
   182   and de_Morgan_conj: "|- (~(P & Q)) <-> (~P | ~Q)"
   183 
   184   and not_iff: "|- ~(P <-> Q) <-> (P <-> ~Q)"
   185   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
   186   done
   187 
   188 lemma imp_cong:
   189   assumes p1: "|- P <-> P'"
   190     and p2: "|- P' ==> |- Q <-> Q'"
   191   shows "|- (P-->Q) <-> (P'-->Q')"
   192   apply (tactic {* lemma_tac @{thm p1} 1 *})
   193   apply (tactic {* safe_tac LK_pack 1 *})
   194    apply (tactic {*
   195      REPEAT (rtac @{thm cut} 1 THEN
   196        DEPTH_SOLVE_1
   197          (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
   198            safe_tac LK_pack 1) *})
   199   done
   200 
   201 lemma conj_cong:
   202   assumes p1: "|- P <-> P'"
   203     and p2: "|- P' ==> |- Q <-> Q'"
   204   shows "|- (P&Q) <-> (P'&Q')"
   205   apply (tactic {* lemma_tac @{thm p1} 1 *})
   206   apply (tactic {* safe_tac LK_pack 1 *})
   207    apply (tactic {*
   208      REPEAT (rtac @{thm cut} 1 THEN
   209        DEPTH_SOLVE_1
   210          (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
   211            safe_tac LK_pack 1) *})
   212   done
   213 
   214 lemma eq_sym_conv: "|- (x=y) <-> (y=x)"
   215   apply (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
   216   done
   217 
   218 use "simpdata.ML"
   219 setup {* Simplifier.map_simpset_global (K LK_ss) *}
   220 
   221 
   222 text {* To create substition rules *}
   223 
   224 lemma eq_imp_subst: "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
   225   apply (tactic {* asm_simp_tac LK_basic_ss 1 *})
   226   done
   227 
   228 lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
   229   apply (rule_tac P = Q in cut)
   230    apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_P}) 2 *})
   231   apply (rule_tac P = "~Q" in cut)
   232    apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_not_P}) 2 *})
   233   apply (tactic {* fast_tac LK_pack 1 *})
   234   done
   235 
   236 lemma if_cancel: "|- (if P then x else x) = x"
   237   apply (tactic {* lemma_tac @{thm split_if} 1 *})
   238   apply (tactic {* fast_tac LK_pack 1 *})
   239   done
   240 
   241 lemma if_eq_cancel: "|- (if x=y then y else x) = x"
   242   apply (tactic {* lemma_tac @{thm split_if} 1 *})
   243   apply (tactic {* safe_tac LK_pack 1 *})
   244   apply (rule symL)
   245   apply (rule basic)
   246   done
   247 
   248 end