0

1 
structure IFOL =


2 
struct


3 


4 
local


5 
val parse_ast_translation = []


6 
val parse_preproc = None


7 
val parse_postproc = None


8 
val parse_translation = []


9 
val print_translation = []


10 
val print_preproc = None


11 
val print_postproc = None


12 
val print_ast_translation = []


13 
in


14 


15 
(**** begin of user section ****)


16 


17 
(**** end of user section ****)


18 


19 
val thy = extend_theory (Pure.thy)


20 
"IFOL"


21 
([("term", ["logic"])],


22 
["term"],


23 
[(["o"], 0)],


24 
[(["o"], ([], "logic"))],


25 
[(["True", "False"], "o")],


26 
Some (NewSext {


27 
mixfix =


28 
[Mixfix("(_)", "o => prop", "Trueprop", [0], 5),


29 
Infixl("=", "['a,'a] => o", 50),


30 
Mixfix("~ _", "o => o", "Not", [40], 40),


31 
Infixr("&", "[o,o] => o", 35),


32 
Infixr("", "[o,o] => o", 30),


33 
Infixr(">", "[o,o] => o", 25),


34 
Infixr("<>", "[o,o] => o", 25),


35 
Binder("ALL ", "('a => o) => o", "All", 0, 10),


36 
Binder("EX ", "('a => o) => o", "Ex", 0, 10),


37 
Binder("EX! ", "('a => o) => o", "Ex1", 0, 10)],


38 
xrules =


39 
[],


40 
parse_ast_translation = parse_ast_translation,


41 
parse_preproc = parse_preproc,


42 
parse_postproc = parse_postproc,


43 
parse_translation = parse_translation,


44 
print_translation = print_translation,


45 
print_preproc = print_preproc,


46 
print_postproc = print_postproc,


47 
print_ast_translation = print_ast_translation}))


48 
[("refl", "a=a"),


49 
("subst", "[ a=b; P(a) ] ==> P(b)"),


50 
("conjI", "[ P; Q ] ==> P&Q"),


51 
("conjunct1", "P&Q ==> P"),


52 
("conjunct2", "P&Q ==> Q"),


53 
("disjI1", "P ==> PQ"),


54 
("disjI2", "Q ==> PQ"),


55 
("disjE", "[ PQ; P ==> R; Q ==> R ] ==> R"),


56 
("impI", "(P ==> Q) ==> P>Q"),


57 
("mp", "[ P>Q; P ] ==> Q"),


58 
("FalseE", "False ==> P"),


59 
("True_def", "True == False>False"),


60 
("not_def", "~P == P>False"),


61 
("iff_def", "P<>Q == (P>Q) & (Q>P)"),


62 
("ex1_def", "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) > y=x)"),


63 
("allI", "(!!x. P(x)) ==> (ALL x.P(x))"),


64 
("spec", "(ALL x.P(x)) ==> P(x)"),


65 
("exI", "P(x) ==> (EX x.P(x))"),


66 
("exE", "[ EX x.P(x); !!x. P(x) ==> R ] ==> R"),


67 
("eq_reflection", "(x=y) ==> (x==y)"),


68 
("iff_reflection", "(P<>Q) ==> (P==Q)")]


69 


70 
val ax = get_axiom thy


71 


72 
val refl = ax "refl"


73 
val subst = ax "subst"


74 
val conjI = ax "conjI"


75 
val conjunct1 = ax "conjunct1"


76 
val conjunct2 = ax "conjunct2"


77 
val disjI1 = ax "disjI1"


78 
val disjI2 = ax "disjI2"


79 
val disjE = ax "disjE"


80 
val impI = ax "impI"


81 
val mp = ax "mp"


82 
val FalseE = ax "FalseE"


83 
val True_def = ax "True_def"


84 
val not_def = ax "not_def"


85 
val iff_def = ax "iff_def"


86 
val ex1_def = ax "ex1_def"


87 
val allI = ax "allI"


88 
val spec = ax "spec"


89 
val exI = ax "exI"


90 
val exE = ax "exE"


91 
val eq_reflection = ax "eq_reflection"


92 
val iff_reflection = ax "iff_reflection"


93 


94 


95 
end


96 
end
