src/Sequents/ILL.thy
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 52143 36ffe23b25f8
child 55228 901a6696cdd8
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
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
22894
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    13
  tens :: "[o, o] => o"        (infixr "><" 35)
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    14
  limp :: "[o, o] => o"        (infixr "-o" 45)
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    15
  liff :: "[o, o] => o"        (infixr "o-o" 45)
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    16
  FShriek :: "o => o"          ("! _" [100] 1000)
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    17
  lconj :: "[o, o] => o"       (infixr "&&" 35)
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    18
  ldisj :: "[o, o] => o"       (infixr "++" 35)
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    19
  zero :: "o"                  ("0")
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    20
  top :: "o"                   ("1")
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    21
  eye :: "o"                   ("I")
619b270607ac eliminated unnamed infixes;
wenzelm
parents: 21588
diff changeset
    22
  aneg :: "o=>o"               ("~_")
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    23
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    24
14765
bafb24c150c1 proper use of 'syntax';
wenzelm
parents: 2073
diff changeset
    25
  (* context manipulation *)
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    26
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    27
 Context      :: "two_seqi"
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    28
14765
bafb24c150c1 proper use of 'syntax';
wenzelm
parents: 2073
diff changeset
    29
  (* promotion rule *)
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    30
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    31
  PromAux :: "three_seqi"
14765
bafb24c150c1 proper use of 'syntax';
wenzelm
parents: 2073
diff changeset
    32
bafb24c150c1 proper use of 'syntax';
wenzelm
parents: 2073
diff changeset
    33
syntax
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 30549
diff changeset
    34
  "_Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
1a0c129bb2e0 modernized translations;
wenzelm
parents: 30549
diff changeset
    35
  "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
1a0c129bb2e0 modernized translations;
wenzelm
parents: 30549
diff changeset
    36
  "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    37
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    38
parse_translation {*
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51309
diff changeset
    39
  [(@{syntax_const "_Trueprop"}, K (single_tr @{const_syntax Trueprop})),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51309
diff changeset
    40
   (@{syntax_const "_Context"}, K (two_seq_tr @{const_syntax Context})),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51309
diff changeset
    41
   (@{syntax_const "_PromAux"}, K (three_seq_tr @{const_syntax PromAux}))]
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 30549
diff changeset
    42
*}
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    43
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    44
print_translation {*
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51309
diff changeset
    45
  [(@{const_syntax Trueprop}, K (single_tr' @{syntax_const "_Trueprop"})),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51309
diff changeset
    46
   (@{const_syntax Context}, K (two_seq_tr' @{syntax_const "_Context"})),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51309
diff changeset
    47
   (@{const_syntax PromAux}, K (three_seq_tr' @{syntax_const "_PromAux"}))]
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 30549
diff changeset
    48
*}
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    49
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    50
defs
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    51
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    52
liff_def:        "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
    53
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    54
aneg_def:        "~A == A -o 0"
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    55
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    56
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    57
axiomatization where
14765
bafb24c150c1 proper use of 'syntax';
wenzelm
parents: 2073
diff changeset
    58
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    59
identity:        "P |- P" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    60
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    61
zerol:           "$G, 0, $H |- A" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    62
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    63
  (* RULES THAT DO NOT DIVIDE CONTEXT *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    64
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    65
derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    66
  (* unfortunately, this one removes !A  *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    67
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    68
contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C" and
14765
bafb24c150c1 proper use of 'syntax';
wenzelm
parents: 2073
diff changeset
    69
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    70
weaken:     "$F, $G |- C ==> $G, !A, $F |- C" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    71
  (* weak form of weakening, in practice just to clean context *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    72
  (* weaken and contract not needed (CHECK)  *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    73
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    74
promote2:        "promaux{ || $H || B} ==> $H |- !B" and
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    75
promote1:        "promaux{!A, $G || $H || B}
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    76
                  ==> promaux {$G || $H, !A || B}" and
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    77
promote0:        "$G |- A ==> promaux {$G || || A}" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    78
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    79
14765
bafb24c150c1 proper use of 'syntax';
wenzelm
parents: 2073
diff changeset
    80
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    81
tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    82
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    83
impr:      "A, $F |- B ==> $F |- A -o B" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    84
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    85
conjr:           "[| $F |- A ;
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    86
                 $F |- B |]
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    87
                ==> $F |- (A && B)" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    88
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    89
conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    90
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    91
conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    92
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    93
disjrl:          "$G |- A ==> $G |- A ++ B" and
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    94
disjrr:          "$G |- B ==> $G |- A ++ B" and
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    95
disjl:           "[| $G, A, $H |- C ;
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    96
                     $G, B, $H |- C |]
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
    97
                 ==> $G, A ++ B, $H |- C" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    98
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
    99
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   100
      (* RULES THAT DIVIDE CONTEXT *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   101
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   102
tensr:           "[| $F, $J :=: $G;
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   103
                     $F |- A ;
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   104
                     $J |- B     |]
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
   105
                     ==> $G |- A >< B" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   106
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   107
impl:            "[| $G, $F :=: $J, $H ;
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   108
                     B, $F |- C ;
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   109
                        $G |- A |]
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
   110
                     ==> $J, A -o B, $H |- C" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   111
14765
bafb24c150c1 proper use of 'syntax';
wenzelm
parents: 2073
diff changeset
   112
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   113
cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   114
          $H1, $H2, $H3, $H4 |- A ;
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
   115
          $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B" and
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   116
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   117
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   118
  (* CONTEXT RULES *)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   119
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
   120
context1:     "$G :=: $G" and
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
   121
context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G" and
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
   122
context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J" and
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
   123
context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G" and
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 42814
diff changeset
   124
context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G" and
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   125
context5:     "$F, $G :=: $H ==> $G, $F :=: $H"
2073
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff changeset
   126
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   127
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   128
ML {*
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   129
val lazy_cs = empty_pack
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   130
  add_safes [@{thm tensl}, @{thm conjr}, @{thm disjl}, @{thm promote0},
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   131
    @{thm context2}, @{thm context3}]
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   132
  add_unsafes [@{thm identity}, @{thm zerol}, @{thm conjll}, @{thm conjlr},
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   133
    @{thm disjrl}, @{thm disjrr}, @{thm impr}, @{thm tensr}, @{thm impl},
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   134
    @{thm derelict}, @{thm weaken}, @{thm promote1}, @{thm promote2},
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   135
    @{thm context1}, @{thm context4a}, @{thm context4b}];
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   136
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   137
fun prom_tac n =
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   138
  REPEAT (resolve_tac [@{thm promote0}, @{thm promote1}, @{thm promote2}] n)
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   139
*}
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   140
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   141
method_setup best_lazy =
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
   142
  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac lazy_cs))) *}
21588
cd0dc678a205 simplified method setup;
wenzelm
parents: 21427
diff changeset
   143
  "lazy classical reasoning"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   144
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   145
lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   146
  apply (rule derelict)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   147
  apply (rule impl)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   148
  apply (rule_tac [2] identity)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   149
  apply (rule context1)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   150
  apply assumption
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   151
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   152
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   153
lemma conj_lemma: " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   154
  apply (rule contract)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   155
  apply (rule_tac A = " (!A) >< (!B) " in cut)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   156
  apply (rule_tac [2] tensr)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   157
  prefer 3
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   158
  apply (subgoal_tac "! (A && B) |- !A")
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   159
  apply assumption
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   160
  apply best_lazy
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   161
  prefer 3
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   162
  apply (subgoal_tac "! (A && B) |- !B")
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   163
  apply assumption
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   164
  apply best_lazy
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   165
  apply (rule_tac [2] context1)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   166
  apply (rule_tac [2] tensl)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   167
  prefer 2 apply (assumption)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   168
  apply (rule context3)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   169
  apply (rule context3)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   170
  apply (rule context1)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   171
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   172
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   173
lemma impr_contract: "!A, !A, $G |- B ==> $G |- (!A) -o B"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   174
  apply (rule impr)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   175
  apply (rule contract)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   176
  apply assumption
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   177
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   178
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   179
lemma impr_contr_der: "A, !A, $G |- B ==> $G |- (!A) -o B"
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 (rule derelict)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   183
  apply assumption
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   184
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   185
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   186
lemma contrad1: "$F, (!B) -o 0, $G, !B, $H |- A"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   187
  apply (rule impl)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   188
  apply (rule_tac [3] identity)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   189
  apply (rule context3)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   190
  apply (rule context1)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   191
  apply (rule zerol)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   192
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   193
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   194
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   195
lemma contrad2: "$F, !B, $G, (!B) -o 0, $H |- A"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   196
  apply (rule impl)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   197
  apply (rule_tac [3] identity)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   198
  apply (rule context3)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   199
  apply (rule context1)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   200
  apply (rule zerol)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   201
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   202
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   203
lemma ll_mp: "A -o B, A |- B"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   204
  apply (rule impl)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   205
  apply (rule_tac [2] identity)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   206
  apply (rule_tac [2] identity)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   207
  apply (rule context1)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   208
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   209
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   210
lemma mp_rule1: "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   211
  apply (rule_tac A = "B" in cut)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   212
  apply (rule_tac [2] ll_mp)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   213
  prefer 2 apply (assumption)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   214
  apply (rule context3)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   215
  apply (rule context3)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   216
  apply (rule context1)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   217
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   218
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   219
lemma mp_rule2: "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   220
  apply (rule_tac A = "B" in cut)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   221
  apply (rule_tac [2] ll_mp)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   222
  prefer 2 apply (assumption)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   223
  apply (rule context3)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   224
  apply (rule context3)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   225
  apply (rule context1)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   226
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   227
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   228
lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   229
  by best_lazy
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   230
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   231
lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==>  
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   232
          $F, !((!(A ++ B)) -o 0), $G |- C"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   233
  apply (rule cut)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   234
  apply (rule_tac [2] or_to_and)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   235
  prefer 2 apply (assumption)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   236
  apply (rule context3)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   237
  apply (rule context1)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   238
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   239
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   240
lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   241
  apply (rule impr)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   242
  apply (rule conj_lemma)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   243
  apply (rule disjl)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   244
  apply (rule mp_rule1, best_lazy)+
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   245
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   246
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   247
lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   248
  by best_lazy
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   249
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   250
lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   251
  apply (rule impr)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   252
  apply (rule contract)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   253
  apply (rule impl)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   254
  apply (rule_tac [3] identity)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   255
  apply (rule context1)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   256
  apply best_lazy
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   257
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   258
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   259
lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   260
  apply (rule_tac A = "!A -o 0" in cut)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   261
  apply (rule_tac [2] a_not_a)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   262
  prefer 2 apply (assumption)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   263
  apply best_lazy
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   264
  done
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   265
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   266
ML {*
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   267
val safe_cs = lazy_cs add_safes [@{thm conj_lemma}, @{thm ll_mp}, @{thm contrad1},
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   268
                                 @{thm contrad2}, @{thm mp_rule1}, @{thm mp_rule2}, @{thm o_a_rule},
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   269
                                 @{thm a_not_a_rule}]
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   270
                      add_unsafes [@{thm aux_impl}];
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   271
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 35113
diff changeset
   272
val power_cs = safe_cs add_unsafes [@{thm impr_contr_der}];
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   273
*}
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   274
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   275
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   276
method_setup best_safe =
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 39159
diff changeset
   277
  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *}
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   278
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   279
method_setup best_power =
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 39159
diff changeset
   280
  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *}
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   281
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   282
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   283
(* Some examples from Troelstra and van Dalen *)
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   284
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   285
lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   286
  by best_safe
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   287
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   288
lemma "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   289
  by best_safe
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   290
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   291
lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |-
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   292
        (!A) -o ( (!  ((!B) -o 0)) -o 0)"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   293
  by best_safe
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   294
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   295
lemma "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) |-
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   296
          (!((! ((!A) -o B) ) -o 0)) -o 0"
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   297
  by best_power
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   298
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 17481
diff changeset
   299
end