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