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 
method_setup auto1 =


33 
{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac safe_cs)) *} ""


34 
method_setup auto2 =


35 
{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac power_cs)) *} ""


36 


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


38 


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


40 
by auto1


41 


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


43 
by auto1


44 


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


46 
by auto1


47 


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


49 
by auto2


50 


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


52 
by auto1


53 


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


55 
by auto2


56 


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


58 
by auto1


59 


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


61 
by auto1


62 


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


64 
by auto1


65 


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


67 
by auto2


68 


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


70 
by auto1


71 


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


73 
by auto1


74 


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


76 
by auto1


77 


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


79 
by auto1


80 


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


82 
by auto1


83 


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


85 
by auto1


86 


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


88 
by auto1


89 


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


91 
by auto1


92 


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


94 
by auto2


95 


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


97 
by auto2


98 


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


100 
by auto1


101 


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


103 
by auto1


104 


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


106 
by auto1


107 


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


109 
by auto1


110 


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


112 
by auto1


113 


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


115 
by auto1


116 


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


118 
by auto2


119 


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


121 
by auto1


122 


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


124 
by auto1


125 


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


127 
by auto1


128 


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


130 
by auto2


131 


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


133 
by auto1


134 


135 
end
