author  wenzelm 
Sun, 21 Feb 2010 20:54:40 +0100  
changeset 35252  24c466b2cdc8 
parent 35054  a5db9779b026 
child 35762  af3ff2ba4c54 
permissions  rwrr 
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) 

35252
24c466b2cdc8
simplified syntax  to make it work for authentic syntax;
wenzelm
parents:
35054
diff
changeset

14 
ff :: "plf" ("ff") 
21426  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*]" 

35252
24c466b2cdc8
simplified syntax  to make it work for authentic syntax;
wenzelm
parents:
35054
diff
changeset

25 
"[*  A *]" == "[*A > ff*]" 
24c466b2cdc8
simplified syntax  to make it work for authentic syntax;
wenzelm
parents:
35054
diff
changeset

26 
"[* ff *]" == "0" 
21426  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 