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 
"@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 
(* from [kleene 52] pp 118,119 *)


33 


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

21427

35 
by best_safe

21426

36 


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

21427

38 
by best_safe

21426

39 


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

21427

41 
by best_safe

21426

42 


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

21427

44 
by best_power

21426

45 


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

21427

47 
by best_safe

21426

48 


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

21427

50 
by best_power

21426

51 


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

21427

53 
by best_safe

21426

54 


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

21427

56 
by best_safe

21426

57 


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

21427

59 
by best_safe

21426

60 


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

21427

62 
by best_power

21426

63 


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

21427

65 
by best_safe

21426

66 


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

21427

68 
by best_safe

21426

69 


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

21427

71 
by best_safe

21426

72 


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

21427

74 
by best_safe

21426

75 


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

21427

77 
by best_safe

21426

78 


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

21427

80 
by best_safe

21426

81 


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

21427

83 
by best_safe

21426

84 


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

21427

86 
by best_safe

21426

87 


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

21427

89 
by best_power

21426

90 


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

21427

92 
by best_power

21426

93 


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

21427

95 
by best_safe

21426

96 


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

21427

98 
by best_safe

21426

99 


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

21427

101 
by best_safe

21426

102 


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

21427

104 
by best_safe

21426

105 


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

21427

107 
by best_safe

21426

108 


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

21427

110 
by best_safe

21426

111 


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

21427

113 
by best_power

21426

114 


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

21427

116 
by best_safe

21426

117 


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

21427

119 
by best_safe

21426

120 


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

21427

122 
by best_safe

21426

123 


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

21427

125 
by best_power

21426

126 


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

21427

128 
by best_safe

21426

129 


130 
end
