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