src/Sequents/LK.thy
changeset 27149 123377499a8e
parent 21428 f84cf8e9cad8
child 28952 15a4b2cf8c34
equal deleted inserted replaced
27148:5b78e50adc49 27149:123377499a8e
    16 theory LK
    16 theory LK
    17 imports LK0
    17 imports LK0
    18 uses ("simpdata.ML")
    18 uses ("simpdata.ML")
    19 begin
    19 begin
    20 
    20 
    21 axioms
    21 axiomatization where
    22 
    22   monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q" and
    23   monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
       
    24 
    23 
    25   left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
    24   left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
    26                ==> (P, $H |- $F) == (P', $H' |- $F')"
    25                ==> (P, $H |- $F) == (P', $H' |- $F')"
    27 
    26 
       
    27 
       
    28 subsection {* Rewrite rules *}
       
    29 
       
    30 lemma conj_simps:
       
    31   "|- P & True <-> P"
       
    32   "|- True & P <-> P"
       
    33   "|- P & False <-> False"
       
    34   "|- False & P <-> False"
       
    35   "|- P & P <-> P"
       
    36   "|- P & P & Q <-> P & Q"
       
    37   "|- P & ~P <-> False"
       
    38   "|- ~P & P <-> False"
       
    39   "|- (P & Q) & R <-> P & (Q & R)"
       
    40   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
    41   done
       
    42 
       
    43 lemma disj_simps:
       
    44   "|- P | True <-> True"
       
    45   "|- True | P <-> True"
       
    46   "|- P | False <-> P"
       
    47   "|- False | P <-> P"
       
    48   "|- P | P <-> P"
       
    49   "|- P | P | Q <-> P | Q"
       
    50   "|- (P | Q) | R <-> P | (Q | R)"
       
    51   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
    52   done
       
    53 
       
    54 lemma not_simps:
       
    55   "|- ~ False <-> True"
       
    56   "|- ~ True <-> False"
       
    57   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
    58   done
       
    59 
       
    60 lemma imp_simps:
       
    61   "|- (P --> False) <-> ~P"
       
    62   "|- (P --> True) <-> True"
       
    63   "|- (False --> P) <-> True"
       
    64   "|- (True --> P) <-> P"
       
    65   "|- (P --> P) <-> True"
       
    66   "|- (P --> ~P) <-> ~P"
       
    67   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
    68   done
       
    69 
       
    70 lemma iff_simps:
       
    71   "|- (True <-> P) <-> P"
       
    72   "|- (P <-> True) <-> P"
       
    73   "|- (P <-> P) <-> True"
       
    74   "|- (False <-> P) <-> ~P"
       
    75   "|- (P <-> False) <-> ~P"
       
    76   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
    77   done
       
    78 
       
    79 lemma quant_simps:
       
    80   "!!P. |- (ALL x. P) <-> P"
       
    81   "!!P. |- (ALL x. x=t --> P(x)) <-> P(t)"
       
    82   "!!P. |- (ALL x. t=x --> P(x)) <-> P(t)"
       
    83   "!!P. |- (EX x. P) <-> P"
       
    84   "!!P. |- (EX x. x=t & P(x)) <-> P(t)"
       
    85   "!!P. |- (EX x. t=x & P(x)) <-> P(t)"
       
    86   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
    87   done
       
    88 
       
    89 
       
    90 subsection {* Miniscoping: pushing quantifiers in *}
       
    91 
       
    92 text {*
       
    93   We do NOT distribute of ALL over &, or dually that of EX over |
       
    94   Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
       
    95   show that this step can increase proof length!
       
    96 *}
       
    97 
       
    98 text {*existential miniscoping*}
       
    99 lemma ex_simps:
       
   100   "!!P Q. |- (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
       
   101   "!!P Q. |- (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
       
   102   "!!P Q. |- (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
       
   103   "!!P Q. |- (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
       
   104   "!!P Q. |- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q"
       
   105   "!!P Q. |- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"
       
   106   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
   107   done
       
   108 
       
   109 text {*universal miniscoping*}
       
   110 lemma all_simps:
       
   111   "!!P Q. |- (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
       
   112   "!!P Q. |- (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
       
   113   "!!P Q. |- (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q"
       
   114   "!!P Q. |- (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"
       
   115   "!!P Q. |- (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
       
   116   "!!P Q. |- (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
       
   117   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
   118   done
       
   119 
       
   120 text {*These are NOT supplied by default!*}
       
   121 lemma distrib_simps:
       
   122   "|- P & (Q | R) <-> P&Q | P&R"
       
   123   "|- (Q | R) & P <-> Q&P | R&P"
       
   124   "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"
       
   125   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
   126   done
       
   127 
       
   128 lemma P_iff_F: "|- ~P ==> |- (P <-> False)"
       
   129   apply (erule thinR [THEN cut])
       
   130   apply (tactic {* fast_tac LK_pack 1 *})
       
   131   done
       
   132 
       
   133 lemmas iff_reflection_F = P_iff_F [THEN iff_reflection, standard]
       
   134 
       
   135 lemma P_iff_T: "|- P ==> |- (P <-> True)"
       
   136   apply (erule thinR [THEN cut])
       
   137   apply (tactic {* fast_tac LK_pack 1 *})
       
   138   done
       
   139 
       
   140 lemmas iff_reflection_T = P_iff_T [THEN iff_reflection, standard]
       
   141 
       
   142 
       
   143 lemma LK_extra_simps:
       
   144   "|- P | ~P"
       
   145   "|- ~P | P"
       
   146   "|- ~ ~ P <-> P"
       
   147   "|- (~P --> P) <-> P"
       
   148   "|- (~P <-> ~Q) <-> (P<->Q)"
       
   149   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
   150   done
       
   151 
       
   152 
       
   153 subsection {* Named rewrite rules *}
       
   154 
       
   155 lemma conj_commute: "|- P&Q <-> Q&P"
       
   156   and conj_left_commute: "|- P&(Q&R) <-> Q&(P&R)"
       
   157   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
   158   done
       
   159 
       
   160 lemmas conj_comms = conj_commute conj_left_commute
       
   161 
       
   162 lemma disj_commute: "|- P|Q <-> Q|P"
       
   163   and disj_left_commute: "|- P|(Q|R) <-> Q|(P|R)"
       
   164   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
   165   done
       
   166 
       
   167 lemmas disj_comms = disj_commute disj_left_commute
       
   168 
       
   169 lemma conj_disj_distribL: "|- P&(Q|R) <-> (P&Q | P&R)"
       
   170   and conj_disj_distribR: "|- (P|Q)&R <-> (P&R | Q&R)"
       
   171 
       
   172   and disj_conj_distribL: "|- P|(Q&R) <-> (P|Q) & (P|R)"
       
   173   and disj_conj_distribR: "|- (P&Q)|R <-> (P|R) & (Q|R)"
       
   174 
       
   175   and imp_conj_distrib: "|- (P --> (Q&R)) <-> (P-->Q) & (P-->R)"
       
   176   and imp_conj: "|- ((P&Q)-->R)   <-> (P --> (Q --> R))"
       
   177   and imp_disj: "|- (P|Q --> R)   <-> (P-->R) & (Q-->R)"
       
   178 
       
   179   and imp_disj1: "|- (P-->Q) | R <-> (P-->Q | R)"
       
   180   and imp_disj2: "|- Q | (P-->R) <-> (P-->Q | R)"
       
   181 
       
   182   and de_Morgan_disj: "|- (~(P | Q)) <-> (~P & ~Q)"
       
   183   and de_Morgan_conj: "|- (~(P & Q)) <-> (~P | ~Q)"
       
   184 
       
   185   and not_iff: "|- ~(P <-> Q) <-> (P <-> ~Q)"
       
   186   apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *})
       
   187   done
       
   188 
       
   189 lemma imp_cong:
       
   190   assumes p1: "|- P <-> P'"
       
   191     and p2: "|- P' ==> |- Q <-> Q'"
       
   192   shows "|- (P-->Q) <-> (P'-->Q')"
       
   193   apply (tactic {* lemma_tac @{thm p1} 1 *})
       
   194   apply (tactic {* safe_tac LK_pack 1 *})
       
   195    apply (tactic {*
       
   196      REPEAT (rtac @{thm cut} 1 THEN
       
   197        DEPTH_SOLVE_1
       
   198          (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
       
   199            safe_tac LK_pack 1) *})
       
   200   done
       
   201 
       
   202 lemma conj_cong:
       
   203   assumes p1: "|- P <-> P'"
       
   204     and p2: "|- P' ==> |- Q <-> Q'"
       
   205   shows "|- (P&Q) <-> (P'&Q')"
       
   206   apply (tactic {* lemma_tac @{thm p1} 1 *})
       
   207   apply (tactic {* safe_tac LK_pack 1 *})
       
   208    apply (tactic {*
       
   209      REPEAT (rtac @{thm cut} 1 THEN
       
   210        DEPTH_SOLVE_1
       
   211          (resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
       
   212            safe_tac LK_pack 1) *})
       
   213   done
       
   214 
       
   215 lemma eq_sym_conv: "|- (x=y) <-> (y=x)"
       
   216   apply (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
       
   217   done
       
   218 
    28 use "simpdata.ML"
   219 use "simpdata.ML"
    29 
   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 
    30 end
   248 end