21426

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 
ff :: "plf"


15 


16 
PL :: "plf => o" ("[* / _ / *]" [] 100)


17 

22895

18 
syntax


19 
"_NG" :: "plf => plf" (" _ " [50] 55)


20 

21426

21 
translations


22 


23 
"[* A & B *]" == "[*A*] && [*B*]"


24 
"[* A  B *]" == "![*A*] ++ ![*B*]"


25 
"[*  A *]" == "[*A > ff*]"


26 
"[* ff *]" == "0"


27 
"[* A = B *]" => "[* (A > B) & (B > A) *]"


28 


29 
"[* A > B *]" == "![*A*] o [*B*]"


30 


31 
(* another translations for linear implication:


32 
"[* A > B *]" == "!([*A*] o [*B*])" *)


33 


34 
(* from [kleene 52] pp 118,119 *)


35 


36 
lemma k49a: " [* A > (  (  A)) *]"

21427

37 
by best_safe

21426

38 


39 
lemma k49b: " [*(  (  (  A))) = (  A)*]"

21427

40 
by best_safe

21426

41 


42 
lemma k49c: " [* (A   A) > (   A = A) *]"

21427

43 
by best_safe

21426

44 


45 
lemma k50a: " [*  (A =  A) *]"

21427

46 
by best_power

21426

47 


48 
lemma k51a: " [*   (A   A) *]"

21427

49 
by best_safe

21426

50 


51 
lemma k51b: " [*   (  A > A) *]"

21427

52 
by best_power

21426

53 


54 
lemma k56a: " [* (A  B) >  ( A &  B) *]"

21427

55 
by best_safe

21426

56 


57 
lemma k56b: " [* (A  B) >  (A & B) *]"

21427

58 
by best_safe

21426

59 


60 
lemma k57a: " [* (A & B) >  (A  B) *]"

21427

61 
by best_safe

21426

62 


63 
lemma k57b: " [* (A & B) > (A  B) *]"

21427

64 
by best_power

21426

65 


66 
lemma k58a: " [* (A > B) >  (A & B) *]"

21427

67 
by best_safe

21426

68 


69 
lemma k58b: " [* (A > B) = (A & B) *]"

21427

70 
by best_safe

21426

71 


72 
lemma k58c: " [*  (A & B) = (  A >  B) *]"

21427

73 
by best_safe

21426

74 


75 
lemma k58d: " [* (  A >  B) =   (A  B) *]"

21427

76 
by best_safe

21426

77 


78 
lemma k58e: "! [*  B > B *]  [* ( A > B) = (A > B) *]"

21427

79 
by best_safe

21426

80 


81 
lemma k58f: "! [*  B > B *]  [* (A > B) =  (A & B) *]"

21427

82 
by best_safe

21426

83 


84 
lemma k58g: " [* ( A > B) >  (A & B) *]"

21427

85 
by best_safe

21426

86 


87 
lemma k59a: " [* (A  B) > (A > B) *]"

21427

88 
by best_safe

21426

89 


90 
lemma k59b: " [* (A > B) >   (A  B) *]"

21427

91 
by best_power

21426

92 


93 
lemma k59c: " [* (A > B) >  (A  B) *]"

21427

94 
by best_power

21426

95 


96 
lemma k60a: " [* (A & B) >  (A > B) *]"

21427

97 
by best_safe

21426

98 


99 
lemma k60b: " [* (A & B) >  (A > B) *]"

21427

100 
by best_safe

21426

101 


102 
lemma k60c: " [* (   A & B) >  (A > B) *]"

21427

103 
by best_safe

21426

104 


105 
lemma k60d: " [* (  A &  B) =  (A > B) *]"

21427

106 
by best_safe

21426

107 


108 
lemma k60e: " [*  (A > B) =  (A  B) *]"

21427

109 
by best_safe

21426

110 


111 
lemma k60f: " [*  (A  B) =   (A & B) *]"

21427

112 
by best_safe

21426

113 


114 
lemma k60g: " [*   (A > B) =  (A & B) *]"

21427

115 
by best_power

21426

116 


117 
lemma k60h: " [*  (A & B) = (A >  B) *]"

21427

118 
by best_safe

21426

119 


120 
lemma k60i: " [* (A >  B) = ( A >  B) *]"

21427

121 
by best_safe

21426

122 


123 
lemma k61a: " [* (A  B) > (A > B) *]"

21427

124 
by best_safe

21426

125 


126 
lemma k61b: " [*  (A  B) =  (A > B) *]"

21427

127 
by best_power

21426

128 


129 
lemma k62a: " [* (A  B) >  (A & B) *]"

21427

130 
by best_safe

21426

131 


132 
end
