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
```