author  wenzelm 
Fri, 18 Jun 2021 15:03:12 +0200  
changeset 73866  66bff50bc5f1 
parent 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 

61386  33 
lemma k49a: "\<turnstile> [* A > (  (  A)) *]" 
21427  34 
by best_safe 
21426  35 

61386  36 
lemma k49b: "\<turnstile> [*(  (  (  A))) = (  A)*]" 
21427  37 
by best_safe 
21426  38 

61386  39 
lemma k49c: "\<turnstile> [* (A   A) > (   A = A) *]" 
21427  40 
by best_safe 
21426  41 

61386  42 
lemma k50a: "\<turnstile> [*  (A =  A) *]" 
21427  43 
by best_power 
21426  44 

61386  45 
lemma k51a: "\<turnstile> [*   (A   A) *]" 
21427  46 
by best_safe 
21426  47 

61386  48 
lemma k51b: "\<turnstile> [*   (  A > A) *]" 
21427  49 
by best_power 
21426  50 

61386  51 
lemma k56a: "\<turnstile> [* (A  B) >  ( A &  B) *]" 
21427  52 
by best_safe 
21426  53 

61386  54 
lemma k56b: "\<turnstile> [* (A  B) >  (A & B) *]" 
21427  55 
by best_safe 
21426  56 

61386  57 
lemma k57a: "\<turnstile> [* (A & B) >  (A  B) *]" 
21427  58 
by best_safe 
21426  59 

61386  60 
lemma k57b: "\<turnstile> [* (A & B) > (A  B) *]" 
21427  61 
by best_power 
21426  62 

61386  63 
lemma k58a: "\<turnstile> [* (A > B) >  (A & B) *]" 
21427  64 
by best_safe 
21426  65 

61386  66 
lemma k58b: "\<turnstile> [* (A > B) = (A & B) *]" 
21427  67 
by best_safe 
21426  68 

61386  69 
lemma k58c: "\<turnstile> [*  (A & B) = (  A >  B) *]" 
21427  70 
by best_safe 
21426  71 

61386  72 
lemma k58d: "\<turnstile> [* (  A >  B) =   (A  B) *]" 
21427  73 
by best_safe 
21426  74 

61386  75 
lemma k58e: "! [*  B > B *] \<turnstile> [* ( A > B) = (A > B) *]" 
21427  76 
by best_safe 
21426  77 

61386  78 
lemma k58f: "! [*  B > B *] \<turnstile> [* (A > B) =  (A & B) *]" 
21427  79 
by best_safe 
21426  80 

61386  81 
lemma k58g: "\<turnstile> [* ( A > B) >  (A & B) *]" 
21427  82 
by best_safe 
21426  83 

61386  84 
lemma k59a: "\<turnstile> [* (A  B) > (A > B) *]" 
21427  85 
by best_safe 
21426  86 

61386  87 
lemma k59b: "\<turnstile> [* (A > B) >   (A  B) *]" 
21427  88 
by best_power 
21426  89 

61386  90 
lemma k59c: "\<turnstile> [* (A > B) >  (A  B) *]" 
21427  91 
by best_power 
21426  92 

61386  93 
lemma k60a: "\<turnstile> [* (A & B) >  (A > B) *]" 
21427  94 
by best_safe 
21426  95 

61386  96 
lemma k60b: "\<turnstile> [* (A & B) >  (A > B) *]" 
21427  97 
by best_safe 
21426  98 

61386  99 
lemma k60c: "\<turnstile> [* (   A & B) >  (A > B) *]" 
21427  100 
by best_safe 
21426  101 

61386  102 
lemma k60d: "\<turnstile> [* (  A &  B) =  (A > B) *]" 
21427  103 
by best_safe 
21426  104 

61386  105 
lemma k60e: "\<turnstile> [*  (A > B) =  (A  B) *]" 
21427  106 
by best_safe 
21426  107 

61386  108 
lemma k60f: "\<turnstile> [*  (A  B) =   (A & B) *]" 
21427  109 
by best_safe 
21426  110 

61386  111 
lemma k60g: "\<turnstile> [*   (A > B) =  (A & B) *]" 
21427  112 
by best_power 
21426  113 

61386  114 
lemma k60h: "\<turnstile> [*  (A & B) = (A >  B) *]" 
21427  115 
by best_safe 
21426  116 

61386  117 
lemma k60i: "\<turnstile> [* (A >  B) = ( A >  B) *]" 
21427  118 
by best_safe 
21426  119 

61386  120 
lemma k61a: "\<turnstile> [* (A  B) > (A > B) *]" 
21427  121 
by best_safe 
21426  122 

61386  123 
lemma k61b: "\<turnstile> [*  (A  B) =  (A > B) *]" 
21427  124 
by best_power 
21426  125 

61386  126 
lemma k62a: "\<turnstile> [* (A  B) >  (A & B) *]" 
21427  127 
by best_safe 
21426  128 

129 
end 