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