src/Sequents/ILL.thy
author wenzelm
Sat Oct 10 20:54:44 2015 +0200 (2015-10-10)
changeset 61386 0a29a984a91b
parent 61385 538100cc4399
child 62144 bdab93ccfaf8
permissions -rw-r--r--
more symbols;
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@61385
    13
  tens :: "[o, o] \<Rightarrow> o"        (infixr "><" 35)
wenzelm@61385
    14
  limp :: "[o, o] \<Rightarrow> o"        (infixr "-o" 45)
wenzelm@61385
    15
  liff :: "[o, o] \<Rightarrow> o"        (infixr "o-o" 45)
wenzelm@61385
    16
  FShriek :: "o \<Rightarrow> o"          ("! _" [100] 1000)
wenzelm@61385
    17
  lconj :: "[o, o] \<Rightarrow> o"       (infixr "&&" 35)
wenzelm@61385
    18
  ldisj :: "[o, o] \<Rightarrow> o"       (infixr "++" 35)
wenzelm@22894
    19
  zero :: "o"                  ("0")
wenzelm@22894
    20
  top :: "o"                   ("1")
wenzelm@22894
    21
  eye :: "o"                   ("I")
wenzelm@61385
    22
  aneg :: "o\<Rightarrow>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@61386
    34
  "_Trueprop" :: "single_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5)
wenzelm@35113
    35
  "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
wenzelm@35113
    36
  "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")
paulson@2073
    37
wenzelm@60770
    38
parse_translation \<open>
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@60770
    42
\<close>
wenzelm@17481
    43
wenzelm@60770
    44
print_translation \<open>
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@60770
    48
\<close>
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@61386
    59
identity:        "P \<turnstile> P" and
paulson@2073
    60
wenzelm@61386
    61
zerol:           "$G, 0, $H \<turnstile> A" and
paulson@2073
    62
paulson@2073
    63
  (* RULES THAT DO NOT DIVIDE CONTEXT *)
paulson@2073
    64
wenzelm@61386
    65
derelict:   "$F, A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and
paulson@2073
    66
  (* unfortunately, this one removes !A  *)
paulson@2073
    67
wenzelm@61386
    68
contract:  "$F, !A, !A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and
wenzelm@14765
    69
wenzelm@61386
    70
weaken:     "$F, $G \<turnstile> C \<Longrightarrow> $G, !A, $F \<turnstile> 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@61386
    74
promote2:        "promaux{ || $H || B} \<Longrightarrow> $H \<turnstile> !B" and
wenzelm@17481
    75
promote1:        "promaux{!A, $G || $H || B}
wenzelm@61385
    76
                  \<Longrightarrow> promaux {$G || $H, !A || B}" and
wenzelm@61386
    77
promote0:        "$G \<turnstile> A \<Longrightarrow> promaux {$G || || A}" and
paulson@2073
    78
paulson@2073
    79
wenzelm@14765
    80
wenzelm@61386
    81
tensl:     "$H, A, B, $G \<turnstile> C \<Longrightarrow> $H, A >< B, $G \<turnstile> C" and
paulson@2073
    82
wenzelm@61386
    83
impr:      "A, $F \<turnstile> B \<Longrightarrow> $F \<turnstile> A -o B" and
paulson@2073
    84
wenzelm@61386
    85
conjr:           "\<lbrakk>$F \<turnstile> A ;
wenzelm@61386
    86
                 $F \<turnstile> B\<rbrakk>
wenzelm@61386
    87
                \<Longrightarrow> $F \<turnstile> (A && B)" and
paulson@2073
    88
wenzelm@61386
    89
conjll:          "$G, A, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and
paulson@2073
    90
wenzelm@61386
    91
conjlr:          "$G, B, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and
paulson@2073
    92
wenzelm@61386
    93
disjrl:          "$G \<turnstile> A \<Longrightarrow> $G \<turnstile> A ++ B" and
wenzelm@61386
    94
disjrr:          "$G \<turnstile> B \<Longrightarrow> $G \<turnstile> A ++ B" and
wenzelm@61386
    95
disjl:           "\<lbrakk>$G, A, $H \<turnstile> C ;
wenzelm@61386
    96
                   $G, B, $H \<turnstile> C\<rbrakk>
wenzelm@61386
    97
                 \<Longrightarrow> $G, A ++ B, $H \<turnstile> C" and
paulson@2073
    98
paulson@2073
    99
paulson@2073
   100
      (* RULES THAT DIVIDE CONTEXT *)
paulson@2073
   101
wenzelm@61385
   102
tensr:           "\<lbrakk>$F, $J :=: $G;
wenzelm@61386
   103
                   $F \<turnstile> A ;
wenzelm@61386
   104
                   $J \<turnstile> B\<rbrakk>
wenzelm@61386
   105
                     \<Longrightarrow> $G \<turnstile> A >< B" and
paulson@2073
   106
wenzelm@61385
   107
impl:            "\<lbrakk>$G, $F :=: $J, $H ;
wenzelm@61386
   108
                   B, $F \<turnstile> C ;
wenzelm@61386
   109
                   $G \<turnstile> A\<rbrakk>
wenzelm@61386
   110
                     \<Longrightarrow> $J, A -o B, $H \<turnstile> C" and
paulson@2073
   111
wenzelm@14765
   112
wenzelm@61385
   113
cut: "\<lbrakk> $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
wenzelm@61386
   114
        $H1, $H2, $H3, $H4 \<turnstile> A ;
wenzelm@61386
   115
        $J1, $J2, A, $J3, $J4 \<turnstile> B\<rbrakk> \<Longrightarrow> $F \<turnstile> B" and
paulson@2073
   116
paulson@2073
   117
paulson@2073
   118
  (* CONTEXT RULES *)
paulson@2073
   119
wenzelm@51309
   120
context1:     "$G :=: $G" and
wenzelm@61385
   121
context2:     "$F, $G :=: $H, !A, $G \<Longrightarrow> $F, A, $G :=: $H, !A, $G" and
wenzelm@61385
   122
context3:     "$F, $G :=: $H, $J \<Longrightarrow> $F, A, $G :=: $H, A, $J" and
wenzelm@61385
   123
context4a:    "$F :=: $H, $G \<Longrightarrow> $F :=: $H, !A, $G" and
wenzelm@61385
   124
context4b:    "$F, $H :=: $G \<Longrightarrow> $F, !A, $H :=: $G" and
wenzelm@61385
   125
context5:     "$F, $G :=: $H \<Longrightarrow> $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@61386
   153
lemma aux_impl: "$F, $G \<turnstile> A \<Longrightarrow> $F, !(A -o B), $G \<turnstile> 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@61386
   161
lemma conj_lemma: " $F, !A, !B, $G \<turnstile> C \<Longrightarrow> $F, !(A && B), $G \<turnstile> 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@61386
   166
  apply (subgoal_tac "! (A && B) \<turnstile> !A")
wenzelm@21427
   167
  apply assumption
wenzelm@55232
   168
  apply best
wenzelm@21427
   169
  prefer 3
wenzelm@61386
   170
  apply (subgoal_tac "! (A && B) \<turnstile> !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@61386
   181
lemma impr_contract: "!A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!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@61386
   187
lemma impr_contr_der: "A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!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@61386
   194
lemma contrad1: "$F, (!B) -o 0, $G, !B, $H \<turnstile> 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@61386
   203
lemma contrad2: "$F, !B, $G, (!B) -o 0, $H \<turnstile> 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@61386
   211
lemma ll_mp: "A -o B, A \<turnstile> 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@61386
   218
lemma mp_rule1: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A, $G, A -o B, $H \<turnstile> 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@61386
   227
lemma mp_rule2: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A -o B, $G, A, $H \<turnstile> 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@61386
   236
lemma or_to_and: "!((!(A ++ B)) -o 0) \<turnstile> !( ((!A) -o 0) && ((!B) -o 0))"
wenzelm@55232
   237
  by best
wenzelm@21427
   238
wenzelm@61386
   239
lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G \<turnstile> C \<Longrightarrow>
wenzelm@61386
   240
          $F, !((!(A ++ B)) -o 0), $G \<turnstile> 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@61386
   248
lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) \<turnstile> (!(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@61386
   255
lemma not_imp: "!A, !((!B) -o 0) \<turnstile> (!((!A) -o B)) -o 0"
wenzelm@55232
   256
  by best
wenzelm@21427
   257
wenzelm@61386
   258
lemma a_not_a: "!A -o (!A -o 0) \<turnstile> !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@61386
   267
lemma a_not_a_rule: "$J1, !A -o 0, $J2 \<turnstile> B \<Longrightarrow> $J1, !A -o (!A -o 0), $J2 \<turnstile> 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@60770
   274
ML \<open>
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@60770
   286
\<close>
wenzelm@21427
   287
wenzelm@21427
   288
method_setup best_safe =
wenzelm@60770
   289
  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack safe_pack ctxt)))\<close>
wenzelm@21427
   290
wenzelm@21427
   291
method_setup best_power =
wenzelm@60770
   292
  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack power_pack ctxt)))\<close>
wenzelm@21427
   293
wenzelm@21427
   294
wenzelm@21427
   295
(* Some examples from Troelstra and van Dalen *)
wenzelm@21427
   296
wenzelm@61386
   297
lemma "!((!A) -o ((!B) -o 0)) \<turnstile> (!(A && B)) -o 0"
wenzelm@21427
   298
  by best_safe
wenzelm@21427
   299
wenzelm@61386
   300
lemma "!((!(A && B)) -o 0) \<turnstile> !((!A) -o ((!B) -o 0))"
wenzelm@21427
   301
  by best_safe
wenzelm@21427
   302
wenzelm@61386
   303
lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) \<turnstile>
wenzelm@21427
   304
        (!A) -o ( (!  ((!B) -o 0)) -o 0)"
wenzelm@21427
   305
  by best_safe
wenzelm@21427
   306
wenzelm@61386
   307
lemma "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) \<turnstile>
wenzelm@21427
   308
          (!((! ((!A) -o B) ) -o 0)) -o 0"
wenzelm@21427
   309
  by best_power
wenzelm@21427
   310
wenzelm@21427
   311
end