author  blanchet 
Mon, 26 Nov 2012 13:35:05 +0100  
changeset 50222  40e3c3be6bca 
parent 35762  af3ff2ba4c54 
child 61385  538100cc4399 
permissions  rwrr 
21426  1 
theory ILL_predlog 
2 
imports ILL 

3 
begin 

4 

5 
typedecl plf 

6 

7 
consts 

8 
conj :: "[plf,plf] => plf" (infixr "&" 35) 

9 
disj :: "[plf,plf] => plf" (infixr "" 35) 

10 
impl :: "[plf,plf] => plf" (infixr ">" 35) 

11 
eq :: "[plf,plf] => plf" (infixr "=" 35) 

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

12 
ff :: "plf" ("ff") 
21426  13 

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

15 

22895  16 
syntax 
17 
"_NG" :: "plf => plf" (" _ " [50] 55) 

18 

21426  19 
translations 
20 

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

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

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

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

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