src/Sequents/ILL_predlog.thy
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 21427 7c8f4a331f9b
child 22895 adc529c89281
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
wenzelm@21426
     1
(* $Id$ *)
wenzelm@21426
     2
wenzelm@21426
     3
theory ILL_predlog
wenzelm@21426
     4
imports ILL
wenzelm@21426
     5
begin
wenzelm@21426
     6
wenzelm@21426
     7
typedecl plf
wenzelm@21426
     8
wenzelm@21426
     9
consts
wenzelm@21426
    10
  conj :: "[plf,plf] => plf"   (infixr "&" 35)
wenzelm@21426
    11
  disj :: "[plf,plf] => plf"   (infixr "|" 35)
wenzelm@21426
    12
  impl :: "[plf,plf] => plf"   (infixr ">" 35)
wenzelm@21426
    13
  eq :: "[plf,plf] => plf"   (infixr "=" 35)
wenzelm@21426
    14
  "@NG" :: "plf => plf"   ("- _ " [50] 55)
wenzelm@21426
    15
  ff    :: "plf"
wenzelm@21426
    16
wenzelm@21426
    17
  PL    :: "plf => o"      ("[* / _ / *]" [] 100)
wenzelm@21426
    18
wenzelm@21426
    19
translations
wenzelm@21426
    20
wenzelm@21426
    21
  "[* A & B *]" == "[*A*] && [*B*]"
wenzelm@21426
    22
  "[* A | B *]" == "![*A*] ++ ![*B*]"
wenzelm@21426
    23
  "[* - A *]"   == "[*A > ff*]"
wenzelm@21426
    24
  "[* ff *]"    == "0"
wenzelm@21426
    25
  "[* A = B *]" => "[* (A > B) & (B > A) *]"
wenzelm@21426
    26
wenzelm@21426
    27
  "[* A > B *]" == "![*A*] -o [*B*]"
wenzelm@21426
    28
wenzelm@21426
    29
(* another translations for linear implication:
wenzelm@21426
    30
  "[* A > B *]" == "!([*A*] -o [*B*])" *)
wenzelm@21426
    31
wenzelm@21426
    32
(* from [kleene 52] pp 118,119 *)
wenzelm@21426
    33
wenzelm@21426
    34
lemma k49a: "|- [* A > ( - ( - A)) *]"
wenzelm@21427
    35
  by best_safe
wenzelm@21426
    36
wenzelm@21426
    37
lemma k49b: "|- [*( - ( - ( - A))) = ( - A)*]"
wenzelm@21427
    38
  by best_safe
wenzelm@21426
    39
wenzelm@21426
    40
lemma k49c: "|- [* (A | - A) > ( - - A = A) *]"
wenzelm@21427
    41
  by best_safe
wenzelm@21426
    42
wenzelm@21426
    43
lemma k50a: "|- [* - (A = - A) *]"
wenzelm@21427
    44
  by best_power
wenzelm@21426
    45
wenzelm@21426
    46
lemma k51a: "|- [* - - (A | - A) *]"
wenzelm@21427
    47
  by best_safe
wenzelm@21426
    48
wenzelm@21426
    49
lemma k51b: "|- [* - - (- - A > A) *]"
wenzelm@21427
    50
  by best_power
wenzelm@21426
    51
wenzelm@21426
    52
lemma k56a: "|- [* (A | B) > - (- A & - B) *]"
wenzelm@21427
    53
  by best_safe
wenzelm@21426
    54
wenzelm@21426
    55
lemma k56b: "|- [* (-A | B) > - (A & -B) *]"
wenzelm@21427
    56
  by best_safe
wenzelm@21426
    57
wenzelm@21426
    58
lemma k57a: "|- [* (A & B) > - (-A | -B) *]"
wenzelm@21427
    59
  by best_safe
wenzelm@21426
    60
wenzelm@21426
    61
lemma k57b: "|- [* (A & -B) > -(-A | B) *]"
wenzelm@21427
    62
  by best_power
wenzelm@21426
    63
wenzelm@21426
    64
lemma k58a: "|- [* (A > B) > - (A & -B) *]"
wenzelm@21427
    65
  by best_safe
wenzelm@21426
    66
wenzelm@21426
    67
lemma k58b: "|- [* (A > -B) = -(A & B) *]"
wenzelm@21427
    68
  by best_safe
wenzelm@21426
    69
wenzelm@21426
    70
lemma k58c: "|- [* - (A & B) = (- - A > - B) *]"
wenzelm@21427
    71
  by best_safe
wenzelm@21426
    72
wenzelm@21426
    73
lemma k58d: "|- [* (- - A > - B) = - - (-A | -B) *]"
wenzelm@21427
    74
  by best_safe
wenzelm@21426
    75
wenzelm@21426
    76
lemma k58e: "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]"
wenzelm@21427
    77
  by best_safe
wenzelm@21426
    78
wenzelm@21426
    79
lemma k58f: "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]"
wenzelm@21427
    80
  by best_safe
wenzelm@21426
    81
wenzelm@21426
    82
lemma k58g: "|- [* (- -A > B) > - (A & -B) *]"
wenzelm@21427
    83
  by best_safe
wenzelm@21426
    84
wenzelm@21426
    85
lemma k59a: "|- [* (-A | B) > (A > B) *]"
wenzelm@21427
    86
  by best_safe
wenzelm@21426
    87
wenzelm@21426
    88
lemma k59b: "|- [* (A > B) > - - (-A | B) *]"
wenzelm@21427
    89
  by best_power
wenzelm@21426
    90
wenzelm@21426
    91
lemma k59c: "|- [* (-A > B) > - -(A | B) *]"
wenzelm@21427
    92
  by best_power
wenzelm@21426
    93
wenzelm@21426
    94
lemma k60a: "|- [* (A & B) > - (A > -B) *]"
wenzelm@21427
    95
  by best_safe
wenzelm@21426
    96
wenzelm@21426
    97
lemma k60b: "|- [* (A & -B) > - (A > B) *]"
wenzelm@21427
    98
  by best_safe
wenzelm@21426
    99
wenzelm@21426
   100
lemma k60c: "|- [* ( - - A & B) > - (A > -B) *]"
wenzelm@21427
   101
  by best_safe
wenzelm@21426
   102
wenzelm@21426
   103
lemma k60d: "|- [* (- - A & - B) = - (A > B) *]"
wenzelm@21427
   104
  by best_safe
wenzelm@21426
   105
wenzelm@21426
   106
lemma k60e: "|- [* - (A > B) = - (-A | B) *]"
wenzelm@21427
   107
  by best_safe
wenzelm@21426
   108
wenzelm@21426
   109
lemma k60f: "|- [* - (-A | B) = - - (A & -B) *]"
wenzelm@21427
   110
  by best_safe
wenzelm@21426
   111
wenzelm@21426
   112
lemma k60g: "|- [* - - (A > B) = - (A & -B) *]"
wenzelm@21427
   113
  by best_power
wenzelm@21426
   114
wenzelm@21426
   115
lemma k60h: "|- [* - (A & -B) = (A > - -B) *]"
wenzelm@21427
   116
  by best_safe
wenzelm@21426
   117
wenzelm@21426
   118
lemma k60i: "|- [* (A > - -B) = (- -A > - -B) *]"
wenzelm@21427
   119
  by best_safe
wenzelm@21426
   120
wenzelm@21426
   121
lemma k61a: "|- [* (A | B) > (-A > B) *]"
wenzelm@21427
   122
  by best_safe
wenzelm@21426
   123
wenzelm@21426
   124
lemma k61b: "|- [* - (A | B) = - (-A > B) *]"
wenzelm@21427
   125
  by best_power
wenzelm@21426
   126
wenzelm@21426
   127
lemma k62a: "|- [* (-A | -B) > - (A & B) *]"
wenzelm@21427
   128
  by best_safe
wenzelm@21426
   129
wenzelm@21426
   130
end