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