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