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