author  wenzelm 
Sat, 10 Oct 2015 20:51:39 +0200  
changeset 61385  538100cc4399 
parent 35762  af3ff2ba4c54 
child 61386  0a29a984a91b 
permissions  rwrr 
21426  1 
theory ILL_predlog 
2 
imports ILL 

3 
begin 

4 

5 
typedecl plf 

6 

7 
consts 

61385  8 
conj :: "[plf,plf] \<Rightarrow> plf" (infixr "&" 35) 
9 
disj :: "[plf,plf] \<Rightarrow> plf" (infixr "" 35) 

10 
impl :: "[plf,plf] \<Rightarrow> plf" (infixr ">" 35) 

11 
eq :: "[plf,plf] \<Rightarrow> 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 

61385  14 
PL :: "plf \<Rightarrow> o" ("[* / _ / *]" [] 100) 
21426  15 

22895  16 
syntax 
61385  17 
"_NG" :: "plf \<Rightarrow> plf" (" _ " [50] 55) 
22895  18 

21426  19 
translations 
61385  20 
"[* A & B *]" \<rightleftharpoons> "[*A*] && [*B*]" 
21 
"[* A  B *]" \<rightleftharpoons> "![*A*] ++ ![*B*]" 

22 
"[*  A *]" \<rightleftharpoons> "[*A > ff*]" 

23 
"[* ff *]" \<rightleftharpoons> "0" 

24 
"[* A = B *]" \<rightharpoonup> "[* (A > B) & (B > A) *]" 

21426  25 

61385  26 
"[* A > B *]" \<rightleftharpoons> "![*A*] o [*B*]" 
21426  27 

28 
(* another translations for linear implication: 

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

30 

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

32 

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

21427  34 
by best_safe 
21426  35 

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

21427  37 
by best_safe 
21426  38 

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

21427  40 
by best_safe 
21426  41 

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

21427  43 
by best_power 
21426  44 

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

21427  46 
by best_safe 
21426  47 

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

21427  49 
by best_power 
21426  50 

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

21427  52 
by best_safe 
21426  53 

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

21427  55 
by best_safe 
21426  56 

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

21427  58 
by best_safe 
21426  59 

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

21427  61 
by best_power 
21426  62 

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

21427  64 
by best_safe 
21426  65 

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

21427  67 
by best_safe 
21426  68 

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

21427  70 
by best_safe 
21426  71 

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

21427  73 
by best_safe 
21426  74 

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

21427  76 
by best_safe 
21426  77 

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

21427  79 
by best_safe 
21426  80 

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

21427  82 
by best_safe 
21426  83 

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

21427  85 
by best_safe 
21426  86 

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

21427  88 
by best_power 
21426  89 

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

21427  91 
by best_power 
21426  92 

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

21427  94 
by best_safe 
21426  95 

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

21427  97 
by best_safe 
21426  98 

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

21427  100 
by best_safe 
21426  101 

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

21427  103 
by best_safe 
21426  104 

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

21427  106 
by best_safe 
21426  107 

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

21427  109 
by best_safe 
21426  110 

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

21427  112 
by best_power 
21426  113 

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

21427  115 
by best_safe 
21426  116 

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

21427  118 
by best_safe 
21426  119 

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

21427  121 
by best_safe 
21426  122 

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

21427  124 
by best_power 
21426  125 

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

21427  127 
by best_safe 
21426  128 

129 
end 