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