src/Sequents/ILL.thy
author haftmann
Fri Jun 19 21:08:07 2009 +0200 (2009-06-19)
changeset 31726 ffd2dc631d88
parent 30549 d2d7874648bd
child 35113 1a0c129bb2e0
permissions -rw-r--r--
merged
     1 (*  Title:      Sequents/ILL.thy
     2     ID:         $Id$
     3     Author:     Sara Kalvala and Valeria de Paiva
     4     Copyright   1995  University of Cambridge
     5 *)
     6 
     7 theory ILL
     8 imports Sequents
     9 begin
    10 
    11 consts
    12   Trueprop       :: "two_seqi"
    13 
    14   tens :: "[o, o] => o"        (infixr "><" 35)
    15   limp :: "[o, o] => o"        (infixr "-o" 45)
    16   liff :: "[o, o] => o"        (infixr "o-o" 45)
    17   FShriek :: "o => o"          ("! _" [100] 1000)
    18   lconj :: "[o, o] => o"       (infixr "&&" 35)
    19   ldisj :: "[o, o] => o"       (infixr "++" 35)
    20   zero :: "o"                  ("0")
    21   top :: "o"                   ("1")
    22   eye :: "o"                   ("I")
    23   aneg :: "o=>o"               ("~_")
    24 
    25 
    26   (* context manipulation *)
    27 
    28  Context      :: "two_seqi"
    29 
    30   (* promotion rule *)
    31 
    32   PromAux :: "three_seqi"
    33 
    34 syntax
    35   "@Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
    36   "@Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
    37   "@PromAux"  :: "three_seqe" ("promaux {_||_||_}")
    38 
    39 parse_translation {*
    40   [("@Trueprop", single_tr "Trueprop"),
    41    ("@Context", two_seq_tr "Context"),
    42    ("@PromAux", three_seq_tr "PromAux")] *}
    43 
    44 print_translation {*
    45   [("Trueprop", single_tr' "@Trueprop"),
    46    ("Context", two_seq_tr'"@Context"),
    47    ("PromAux", three_seq_tr'"@PromAux")] *}
    48 
    49 defs
    50 
    51 liff_def:        "P o-o Q == (P -o Q) >< (Q -o P)"
    52 
    53 aneg_def:        "~A == A -o 0"
    54 
    55 
    56 axioms
    57 
    58 identity:        "P |- P"
    59 
    60 zerol:           "$G, 0, $H |- A"
    61 
    62   (* RULES THAT DO NOT DIVIDE CONTEXT *)
    63 
    64 derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C"
    65   (* unfortunately, this one removes !A  *)
    66 
    67 contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
    68 
    69 weaken:     "$F, $G |- C ==> $G, !A, $F |- C"
    70   (* weak form of weakening, in practice just to clean context *)
    71   (* weaken and contract not needed (CHECK)  *)
    72 
    73 promote2:        "promaux{ || $H || B} ==> $H |- !B"
    74 promote1:        "promaux{!A, $G || $H || B}
    75                   ==> promaux {$G || $H, !A || B}"
    76 promote0:        "$G |- A ==> promaux {$G || || A}"
    77 
    78 
    79 
    80 tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
    81 
    82 impr:      "A, $F |- B ==> $F |- A -o B"
    83 
    84 conjr:           "[| $F |- A ;
    85                  $F |- B |]
    86                 ==> $F |- (A && B)"
    87 
    88 conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C"
    89 
    90 conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C"
    91 
    92 disjrl:          "$G |- A ==> $G |- A ++ B"
    93 disjrr:          "$G |- B ==> $G |- A ++ B"
    94 disjl:           "[| $G, A, $H |- C ;
    95                      $G, B, $H |- C |]
    96                  ==> $G, A ++ B, $H |- C"
    97 
    98 
    99       (* RULES THAT DIVIDE CONTEXT *)
   100 
   101 tensr:           "[| $F, $J :=: $G;
   102                      $F |- A ;
   103                      $J |- B     |]
   104                      ==> $G |- A >< B"
   105 
   106 impl:            "[| $G, $F :=: $J, $H ;
   107                      B, $F |- C ;
   108                         $G |- A |]
   109                      ==> $J, A -o B, $H |- C"
   110 
   111 
   112 cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
   113           $H1, $H2, $H3, $H4 |- A ;
   114           $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"
   115 
   116 
   117   (* CONTEXT RULES *)
   118 
   119 context1:     "$G :=: $G"
   120 context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
   121 context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
   122 context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
   123 context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
   124 context5:     "$F, $G :=: $H ==> $G, $F :=: $H"
   125 
   126 
   127 ML {*
   128 
   129 val lazy_cs = empty_pack
   130   add_safes [thm "tensl", thm "conjr", thm "disjl", thm "promote0",
   131     thm "context2", thm "context3"]
   132   add_unsafes [thm "identity", thm "zerol", thm "conjll", thm "conjlr",
   133     thm "disjrl", thm "disjrr", thm "impr", thm "tensr", thm "impl",
   134     thm "derelict", thm "weaken", thm "promote1", thm "promote2",
   135     thm "context1", thm "context4a", thm "context4b"];
   136 
   137 local
   138   val promote0 = thm "promote0"
   139   val promote1 = thm "promote1"
   140   val promote2 = thm "promote2"
   141 in
   142 
   143 fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n)
   144 
   145 end
   146 *}
   147 
   148 method_setup best_lazy =
   149   {* Scan.succeed (K (SIMPLE_METHOD' (best_tac lazy_cs))) *}
   150   "lazy classical reasoning"
   151 
   152 lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
   153   apply (rule derelict)
   154   apply (rule impl)
   155   apply (rule_tac [2] identity)
   156   apply (rule context1)
   157   apply assumption
   158   done
   159 
   160 lemma conj_lemma: " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"
   161   apply (rule contract)
   162   apply (rule_tac A = " (!A) >< (!B) " in cut)
   163   apply (rule_tac [2] tensr)
   164   prefer 3
   165   apply (subgoal_tac "! (A && B) |- !A")
   166   apply assumption
   167   apply best_lazy
   168   prefer 3
   169   apply (subgoal_tac "! (A && B) |- !B")
   170   apply assumption
   171   apply best_lazy
   172   apply (rule_tac [2] context1)
   173   apply (rule_tac [2] tensl)
   174   prefer 2 apply (assumption)
   175   apply (rule context3)
   176   apply (rule context3)
   177   apply (rule context1)
   178   done
   179 
   180 lemma impr_contract: "!A, !A, $G |- B ==> $G |- (!A) -o B"
   181   apply (rule impr)
   182   apply (rule contract)
   183   apply assumption
   184   done
   185 
   186 lemma impr_contr_der: "A, !A, $G |- B ==> $G |- (!A) -o B"
   187   apply (rule impr)
   188   apply (rule contract)
   189   apply (rule derelict)
   190   apply assumption
   191   done
   192 
   193 lemma contrad1: "$F, (!B) -o 0, $G, !B, $H |- A"
   194   apply (rule impl)
   195   apply (rule_tac [3] identity)
   196   apply (rule context3)
   197   apply (rule context1)
   198   apply (rule zerol)
   199   done
   200 
   201 
   202 lemma contrad2: "$F, !B, $G, (!B) -o 0, $H |- A"
   203   apply (rule impl)
   204   apply (rule_tac [3] identity)
   205   apply (rule context3)
   206   apply (rule context1)
   207   apply (rule zerol)
   208   done
   209 
   210 lemma ll_mp: "A -o B, A |- B"
   211   apply (rule impl)
   212   apply (rule_tac [2] identity)
   213   apply (rule_tac [2] identity)
   214   apply (rule context1)
   215   done
   216 
   217 lemma mp_rule1: "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"
   218   apply (rule_tac A = "B" in cut)
   219   apply (rule_tac [2] ll_mp)
   220   prefer 2 apply (assumption)
   221   apply (rule context3)
   222   apply (rule context3)
   223   apply (rule context1)
   224   done
   225 
   226 lemma mp_rule2: "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"
   227   apply (rule_tac A = "B" in cut)
   228   apply (rule_tac [2] ll_mp)
   229   prefer 2 apply (assumption)
   230   apply (rule context3)
   231   apply (rule context3)
   232   apply (rule context1)
   233   done
   234 
   235 lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
   236   by best_lazy
   237 
   238 lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==>  
   239           $F, !((!(A ++ B)) -o 0), $G |- C"
   240   apply (rule cut)
   241   apply (rule_tac [2] or_to_and)
   242   prefer 2 apply (assumption)
   243   apply (rule context3)
   244   apply (rule context1)
   245   done
   246 
   247 lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
   248   apply (rule impr)
   249   apply (rule conj_lemma)
   250   apply (rule disjl)
   251   apply (rule mp_rule1, best_lazy)+
   252   done
   253 
   254 lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0"
   255   by best_lazy
   256 
   257 lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0"
   258   apply (rule impr)
   259   apply (rule contract)
   260   apply (rule impl)
   261   apply (rule_tac [3] identity)
   262   apply (rule context1)
   263   apply best_lazy
   264   done
   265 
   266 lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"
   267   apply (rule_tac A = "!A -o 0" in cut)
   268   apply (rule_tac [2] a_not_a)
   269   prefer 2 apply (assumption)
   270   apply best_lazy
   271   done
   272 
   273 ML {*
   274 
   275 val safe_cs = lazy_cs add_safes [thm "conj_lemma", thm "ll_mp", thm "contrad1",
   276                                  thm "contrad2", thm "mp_rule1", thm "mp_rule2", thm "o_a_rule",
   277                                  thm "a_not_a_rule"]
   278                       add_unsafes [thm "aux_impl"];
   279 
   280 val power_cs = safe_cs add_unsafes [thm "impr_contr_der"];
   281 *}
   282 
   283 
   284 method_setup best_safe =
   285   {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *} ""
   286 
   287 method_setup best_power =
   288   {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *} ""
   289 
   290 
   291 (* Some examples from Troelstra and van Dalen *)
   292 
   293 lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0"
   294   by best_safe
   295 
   296 lemma "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))"
   297   by best_safe
   298 
   299 lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |-
   300         (!A) -o ( (!  ((!B) -o 0)) -o 0)"
   301   by best_safe
   302 
   303 lemma "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) |-
   304           (!((! ((!A) -o B) ) -o 0)) -o 0"
   305   by best_power
   306 
   307 end