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