src/Sequents/ILL_predlog.thy
author wenzelm
Sat, 10 Oct 2015 20:54:44 +0200
changeset 61386 0a29a984a91b
parent 61385 538100cc4399
permissions -rw-r--r--
more symbols;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     1
theory ILL_predlog
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     2
imports ILL
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     3
begin
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     4
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     5
typedecl plf
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     6
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     7
consts
61385
538100cc4399 more symbols;
wenzelm
parents: 35762
diff changeset
     8
  conj :: "[plf,plf] \<Rightarrow> plf"   (infixr "&" 35)
538100cc4399 more symbols;
wenzelm
parents: 35762
diff changeset
     9
  disj :: "[plf,plf] \<Rightarrow> plf"   (infixr "|" 35)
538100cc4399 more symbols;
wenzelm
parents: 35762
diff changeset
    10
  impl :: "[plf,plf] \<Rightarrow> plf"   (infixr ">" 35)
538100cc4399 more symbols;
wenzelm
parents: 35762
diff changeset
    11
  eq :: "[plf,plf] \<Rightarrow> plf"   (infixr "=" 35)
35252
24c466b2cdc8 simplified syntax -- to make it work for authentic syntax;
wenzelm
parents: 35054
diff changeset
    12
  ff :: "plf"    ("ff")
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    13
61385
538100cc4399 more symbols;
wenzelm
parents: 35762
diff changeset
    14
  PL    :: "plf \<Rightarrow> o"      ("[* / _ / *]" [] 100)
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    15
22895
adc529c89281 tuned syntax;
wenzelm
parents: 21427
diff changeset
    16
syntax
61385
538100cc4399 more symbols;
wenzelm
parents: 35762
diff changeset
    17
  "_NG" :: "plf \<Rightarrow> plf"   ("- _ " [50] 55)
22895
adc529c89281 tuned syntax;
wenzelm
parents: 21427
diff changeset
    18
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    19
translations
61385
538100cc4399 more symbols;
wenzelm
parents: 35762
diff changeset
    20
  "[* A & B *]" \<rightleftharpoons> "[*A*] && [*B*]"
538100cc4399 more symbols;
wenzelm
parents: 35762
diff changeset
    21
  "[* A | B *]" \<rightleftharpoons> "![*A*] ++ ![*B*]"
538100cc4399 more symbols;
wenzelm
parents: 35762
diff changeset
    22
  "[* - A *]" \<rightleftharpoons> "[*A > ff*]"
538100cc4399 more symbols;
wenzelm
parents: 35762
diff changeset
    23
  "[* ff *]" \<rightleftharpoons> "0"
538100cc4399 more symbols;
wenzelm
parents: 35762
diff changeset
    24
  "[* A = B *]" \<rightharpoonup> "[* (A > B) & (B > A) *]"
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    25
61385
538100cc4399 more symbols;
wenzelm
parents: 35762
diff changeset
    26
  "[* A > B *]" \<rightleftharpoons> "![*A*] -o [*B*]"
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    27
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    28
(* another translations for linear implication:
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    29
  "[* A > B *]" == "!([*A*] -o [*B*])" *)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    30
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    31
(* from [kleene 52] pp 118,119 *)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    32
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    33
lemma k49a: "\<turnstile> [* A > ( - ( - A)) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    34
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    35
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    36
lemma k49b: "\<turnstile> [*( - ( - ( - A))) = ( - A)*]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    37
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    38
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    39
lemma k49c: "\<turnstile> [* (A | - A) > ( - - A = A) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    40
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    41
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    42
lemma k50a: "\<turnstile> [* - (A = - A) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    43
  by best_power
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    44
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    45
lemma k51a: "\<turnstile> [* - - (A | - A) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    46
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    47
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    48
lemma k51b: "\<turnstile> [* - - (- - A > A) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    49
  by best_power
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    50
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    51
lemma k56a: "\<turnstile> [* (A | B) > - (- A & - B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    52
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    53
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    54
lemma k56b: "\<turnstile> [* (-A | B) > - (A & -B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    55
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    56
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    57
lemma k57a: "\<turnstile> [* (A & B) > - (-A | -B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    58
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    59
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    60
lemma k57b: "\<turnstile> [* (A & -B) > -(-A | B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    61
  by best_power
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    62
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    63
lemma k58a: "\<turnstile> [* (A > B) > - (A & -B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    64
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    65
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    66
lemma k58b: "\<turnstile> [* (A > -B) = -(A & B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    67
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    68
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    69
lemma k58c: "\<turnstile> [* - (A & B) = (- - A > - B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    70
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    71
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    72
lemma k58d: "\<turnstile> [* (- - A > - B) = - - (-A | -B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    73
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    74
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    75
lemma k58e: "! [* - -B > B *] \<turnstile> [* (- -A > B) = (A > B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    76
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    77
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    78
lemma k58f: "! [* - -B > B *] \<turnstile> [* (A > B) = - (A & -B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    79
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    80
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    81
lemma k58g: "\<turnstile> [* (- -A > B) > - (A & -B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    82
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    83
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    84
lemma k59a: "\<turnstile> [* (-A | B) > (A > B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    85
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    86
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    87
lemma k59b: "\<turnstile> [* (A > B) > - - (-A | B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    88
  by best_power
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    89
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    90
lemma k59c: "\<turnstile> [* (-A > B) > - -(A | B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    91
  by best_power
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    92
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    93
lemma k60a: "\<turnstile> [* (A & B) > - (A > -B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    94
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    95
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    96
lemma k60b: "\<turnstile> [* (A & -B) > - (A > B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
    97
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    98
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
    99
lemma k60c: "\<turnstile> [* ( - - A & B) > - (A > -B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
   100
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   101
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   102
lemma k60d: "\<turnstile> [* (- - A & - B) = - (A > B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
   103
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   104
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   105
lemma k60e: "\<turnstile> [* - (A > B) = - (-A | B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
   106
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   107
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   108
lemma k60f: "\<turnstile> [* - (-A | B) = - - (A & -B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
   109
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   110
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   111
lemma k60g: "\<turnstile> [* - - (A > B) = - (A & -B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
   112
  by best_power
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   113
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   114
lemma k60h: "\<turnstile> [* - (A & -B) = (A > - -B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
   115
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   116
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   117
lemma k60i: "\<turnstile> [* (A > - -B) = (- -A > - -B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
   118
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   119
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   120
lemma k61a: "\<turnstile> [* (A | B) > (-A > B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
   121
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   122
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   123
lemma k61b: "\<turnstile> [* - (A | B) = - (-A > B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
   124
  by best_power
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   125
61386
0a29a984a91b more symbols;
wenzelm
parents: 61385
diff changeset
   126
lemma k62a: "\<turnstile> [* (-A | -B) > - (A & B) *]"
21427
7c8f4a331f9b converted legacy ML scripts;
wenzelm
parents: 21426
diff changeset
   127
  by best_safe
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   128
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   129
end