%============================================================================== %----Procedures for writing out THF in Isabelle format %---- %----Written by Geoff Sutcliffe January 2009 %============================================================================== %------------------------------------------------------------------------------ isabelle_dequote_ascii([],[]). %----Keep alphanumeric isabelle_dequote_ascii([First|Rest],[First|DequotedRest]):- ( ( First >= 97, First =< 122 ) ; ( First >= 65, First =< 90 ) ; ( First >= 48, First =< 57 ) ), !, isabelle_dequote_ascii(Rest,DequotedRest). %----Cannot end in _, so add a z isabelle_dequote_ascii([_],[95,122]):- !. %----Change everything else to _ isabelle_dequote_ascii([_|Rest],[95|DequotedRest]):- isabelle_dequote_ascii(Rest,DequotedRest). %------------------------------------------------------------------------------ isabelle_dequote(Functor,DequotedFunctor):- name(Functor,ASCII), isabelle_dequote_ascii(ASCII,DequotedASCII), name(DequotedFunctor,DequotedASCII). %------------------------------------------------------------------------------ tptp_to_isabelle(variable,Variable,Variable):- var(Variable), !, write(Variable). tptp_to_isabelle(symbol,Integer,TypedInteger):- integer(Integer), !, name(Integer,IntegerASCII), tptp2X_append("(",IntegerASCII,PreBracketedASCII), tptp2X_append(PreBracketedASCII,"::int",TypedASCII), tptp2X_append(TypedASCII,")",BracketedASCII), name(TypedInteger,BracketedASCII). tptp_to_isabelle(_,TPTP,Isabelle):- tptp2X_member(TPTP,[ %----Lexicon 'ALL','CHR','CONST','EX','GREATEST','INF','INT','Int','LEAST','O','OFCLASS', 'OO','PROD','PROP','SIGMA','SOME','SUM','SUP','THE','TYPE','UN','Un','WRT', 'XCONST']), !, name(TPTP,TPTPASCII), tptp2X_append("TPTP_",TPTPASCII,IsabelleASCII), name(Isabelle,IsabelleASCII). tptp_to_isabelle(_,TPTP,Isabelle):- tptp2X_member(TPTP,[ %----Isabelle reserved words bool,not,the,all,ex,ex1,not_equal,iff, %----Isabelle commands prop,pwd,quit,redo,refute,remove_thy,term,thm,thm_deps,thy_deps, touch_child_thys,touch_thy,typ,undo,undos_proof,unused_thms,use_thy,value, welcome, %----Isabelle lexicon case,div,dvd,else,if,in,let,mem,mod,o,o_m,of,op,respects,respects2,then ]), !, name(TPTP,TPTPASCII), tptp2X_append("tptp_",TPTPASCII,IsabelleASCII), name(Isabelle,IsabelleASCII). %----Catch connective terms first tptp_to_isabelle(symbol,TPTP,Isabelle):- tptp2X_member(ti(TPTP,Isabelle),[ ti('&','(op &)'), ti('|','(op |)'), ti('=>','(op -->)'), ti('<=','(op <--)'), ti('<=>','(op <->)'), ti('=','(op =)'), ti('!=','(op ~=)'), ti('~','Not'), ti('$less','(op <)'), ti('$lesseq','(op <=)'), ti('$greater','(op >)'), ti('$greatereq','(op >=)'), ti('$uminus','(op -)'), ti('$sum','(op +)'), ti('$difference','(op -)'), ti('$product','(op *)'), ti('$is_int','is_int'), ti('$is_rat','is_rat'), ti('$to_int','is_int'), ti('$to_rat','is_rat'), ti('$to_real','is_real') ]), !. tptp_to_isabelle(connective,TPTP,Isabelle):- tptp2X_member(ti(TPTP,Isabelle),[ ti('!','ALL'), ti('?','EX'), ti('^','%'), ti('&','&'), ti('|','|'), ti('=>','-->'), ti('<=','<--'), ti('<=>','<->'), ti('@',''), ti('$tptp_equal','='), ti('$tptp_not_equal','~='), ti('>','=>'), ti('~','~') ]), !. tptp_to_isabelle(_,TPTP,Isabelle):- tptp2X_member(ti(TPTP,Isabelle),[ %----Individuals are translated to a type variable ti('$i','\'i'), ti('$o',bool), ti('$false','False'), ti('$true','True'), ti('$int',int), ti('$rat',rat), ti('$real',real) ]), !. %----If it starts with a dollar, no quotes tptp_to_isabelle(_,DefinedSymbol,DefinedSymbol):- name(DefinedSymbol,[36|_]), !. tptp_to_isabelle(_,Symbol,DequotedSymbol):- isabelle_dequote(Symbol,DequotedSymbol). %------------------------------------------------------------------------------ output_isabelle_formula(Variable,Indent,AlreadyIndented):- looks_like_a_prolog_variable(Variable), !, output_indent(Indent,AlreadyIndented), tptp_to_isabelle(variable,Variable,IsabelleVariable), write(IsabelleVariable). output_isabelle_formula(QuantifiedManyVarsFormula,Indent,AlreadyIndented):- quantified_formula(tptp,QuantifiedManyVarsFormula,Quantifier, [OneVariable,TwoVariables|MoreVariables],QuantifiedFormula,_,_,_,_,_), !, InnerQuantifier =.. [Quantifier,[TwoVariables|MoreVariables]], InnerFormula =.. [:,InnerQuantifier,QuantifiedFormula], OuterQuantifier =.. [Quantifier,[OneVariable]], QuantifiedOneVarFormula =.. [:,OuterQuantifier,InnerFormula], output_isabelle_formula(QuantifiedOneVarFormula,Indent,AlreadyIndented). %----Quantified formula output_isabelle_formula(QuantifiedFormula,Indent,AlreadyIndented):- quantified_formula(tptp,QuantifiedFormula,Quantifier,[Variable],Formula, _,_,_,_,_), !, output_indent(Indent,AlreadyIndented), write('( '), tptp_to_isabelle(connective,Quantifier,IsabelleQuantifier), write(IsabelleQuantifier), write(' '), output_isabelle_formula(Variable,Indent,Indent), write('.'), nl, NewIndent is Indent + 2, output_isabelle_formula(Formula,NewIndent,0), write(' )'). %----Variable types output_isabelle_formula(Variable:Type,Indent,AlreadyIndented):- looks_like_a_variable(Variable), !, output_indent(Indent,AlreadyIndented), output_isabelle_formula(Variable,Indent,Indent), write('::'), output_isabelle_formula(Type,Indent,Indent). %----Binary formula that Isabelle doesn't know output_isabelle_formula(LHS <~> RHS,Indent,AlreadyIndented):- !, output_isabelle_formula(~ (LHS <=> RHS),Indent,AlreadyIndented). output_isabelle_formula(LHS <= RHS,Indent,AlreadyIndented):- !, output_isabelle_formula(RHS => LHS,Indent,AlreadyIndented). %----Binary formula output_isabelle_formula(BinaryFormula,Indent,AlreadyIndented):- binary_formula(tptp,BinaryFormula,Connective,LHS,RHS,_,_,_,_), !, output_indent(Indent,AlreadyIndented), NewIndent is Indent + 2, write('( '), output_isabelle_formula(LHS,NewIndent,NewIndent), nl, output_indent(Indent,0), tptp_to_isabelle(connective,Connective,IsabelleConnective), write(IsabelleConnective), write(' '), output_isabelle_formula(RHS,NewIndent,NewIndent), write(' )'). output_isabelle_formula(~'$tptp_equal'(LHS,RHS),Indent,AlreadyIndented):- !, output_isabelle_formula('$tptp_not_equal'(LHS,RHS),Indent,AlreadyIndented). %----Unary formula output_isabelle_formula(UnaryFormula,Indent,AlreadyIndented):- unary_formula(tptp,UnaryFormula,Connective,Formula,_,_,_), !, output_indent(Indent,AlreadyIndented), NewIndent is Indent + 4, write('( '), tptp_to_isabelle(connective,Connective,IsabelleConnective), write(IsabelleConnective), write(' '), output_isabelle_formula(Formula,NewIndent,NewIndent), write(' )'). %----Equality output_isabelle_formula(Equality,Indent,AlreadyIndented):- Equality =.. [Connective,LHS,RHS], tptp2X_member(Connective,['$tptp_equal','$tptp_not_equal']), !, output_indent(Indent,AlreadyIndented), NewIndent is Indent + 2, write('( '), output_isabelle_formula(LHS,NewIndent,NewIndent), nl, output_indent(Indent,0), tptp_to_isabelle(connective,Connective,IsabelleConnective), write(IsabelleConnective), write(' '), output_isabelle_formula(RHS,NewIndent,NewIndent), write(' )'). %----Symbols output_isabelle_formula(Atomic,Indent,AlreadyIndented):- atomic(Atomic), !, output_indent(Indent,AlreadyIndented), tptp_to_isabelle(symbol,Atomic,IsabelleAtomic), write(IsabelleAtomic). output_isabelle_formula(Unknown,_Indent,_AlreadyIndented):- nl, write('ERROR : Dont know what to do with '), write(Unknown), nl. %------------------------------------------------------------------------------ output_isabelle_annotated_formula(AnnotatedFormula):- AnnotatedFormula =.. [_,_,type,Type: '$tType'|_], !, write('typedecl "'), tptp_to_isabelle(symbol,Type,DequotedType), write(DequotedType), write('"'), nl. output_isabelle_annotated_formula(AnnotatedFormula):- AnnotatedFormula =.. [_,_,type,Symbol:Type|_], !, write(' fixes "'), tptp_to_isabelle(symbol,Symbol,DequotedSymbol), write(DequotedSymbol), write('" :: "'), nl, output_isabelle_formula(Type,4,0), nl, write(' "'), nl. output_isabelle_annotated_formula(AnnotatedFormula):- AnnotatedFormula =.. [_,Name,conjecture,Formula|_], !, write('(* This is the '), %----Hack to hide "This is the conjecture from SystemOnTPTP when $false ( Formula == '$false' -> write('dummy ') ; true ), write('conjecture *)'), nl, write(' shows (* "'), write(Name), write('": *) "'), nl, output_isabelle_formula(Formula,4,0), nl, write(' "'), nl. output_isabelle_annotated_formula(AnnotatedFormula):- AnnotatedFormula =.. [_,Name,_,Formula|_], write(' assumes "'), write(Name), write('": "'), nl, output_isabelle_formula(Formula,4,0), nl, write(' "'), nl. %------------------------------------------------------------------------------ output_isabelle_annotated_formulae([]). output_isabelle_annotated_formulae([FirstFormula|RestOfFormulae]):- output_isabelle_annotated_formula(FirstFormula), nl, output_isabelle_annotated_formulae(RestOfFormulae). %------------------------------------------------------------------------------ select_isabelle_typedecls(TSTPFormulae,[TypeDecl|RestOfTypeDecls], AxiomsAndConjecture):- tptp2X_select(TypeDecl,TSTPFormulae,RestOfTSTPFormulae), TypeDecl =.. [_,_,type,_Type: '$tType'|_], !, select_isabelle_typedecls(RestOfTSTPFormulae,RestOfTypeDecls, AxiomsAndConjecture). select_isabelle_typedecls(TSTPFormulae,[],TSTPFormulae). %------------------------------------------------------------------------------ select_isabelle_axioms_and_conjecture(TSTPFormulae,Axioms,Conjecture):- tptp2X_select(Conjecture,TSTPFormulae,Axioms), Conjecture =.. [thf,_,conjecture|_], !. select_isabelle_axioms_and_conjecture(TSTPFormulae,TSTPFormulae, thf(prove_false,conjecture,'$false')). %------------------------------------------------------------------------------ output_isabelle_header:- write('theory THEORYNAME'),nl, write('imports "~~/src/HOL/Library/TPTP"'),nl, write('begin'),nl, write('ML {* proofs := PROOFMODE *}'),nl, nl. %------------------------------------------------------------------------------ output_isabelle_trailer(Mode,Conjecture):- tptp2X_member(Mode,[refute,nitpick]), !, write(' apply (insert assms)'),nl, write(' apply clarsimp'),nl, write(' '), ( Mode == refute -> write('refute [maxtime = CPULIMIT, expect = genuine, no_assms]') ; write('nitpick [timeout = CPULIMIT, card = 1-10, verbose, expect = genuine, dont_box, no_assms]') %----"expect = genuine" makes sure that an error is generated if the file is %----empty (no models for an empty file). ), nl, write(' oops'),nl, nl, write(' ML_command {* writeln ("% SZS status '), ( Conjecture = thf(_,conjecture,'$false') -> write('Satisfiable') ; write('CounterSatisfiable') ), write(' for FILENAME'), write(' : " ^ Context.theory_name @{theory}) *}'), nl, write('end'),nl. output_isabelle_trailer(sledgehammer,Conjecture):- write(' apply (insert assms)'),nl, %----Run each of the modes for some amount of time write(' apply (tactic {* isabellep_tac @{context} @{claset} @{simpset} @{clasimpset} CPULIMIT *})'),nl, write(' done'),nl, write(' prf THEORYNAME'),nl, write(' ML_command {* writeln ("% SZS status '), ( Conjecture = thf(_,conjecture,'$false') -> write('Unsatisfiable') ; write('Theorem') ), write(' for FILENAME'), write(' : " ^ Context.theory_name @{theory}) *}'), nl, write(' ML_command {* writeln ("% SZS output start Proof for FILENAME") *}'), nl, write(' prf THEORYNAME'), nl, write(' ML_command {* writeln ("% SZS output end Proof for FILENAME") *}'), nl, write('end'),nl. %------------------------------------------------------------------------------ isabelle(isabelle:_,Clauses,_):- tptp_clauses(Clauses), !, write('%----CNF format not available for Isabelle'), nl. isabelle(isabelle:Mode,Formulae,_FileHeader):- tptp_formulae(Formulae), !, convert_formulae_to_tptp(Formulae,TSTPFormulae), select_isabelle_typedecls(TSTPFormulae,TypeDecls,AxiomsAndConjecture), output_isabelle_header, output_isabelle_annotated_formulae(TypeDecls), write('lemma THEORYNAME:'),nl, select_isabelle_axioms_and_conjecture(AxiomsAndConjecture,Axioms, Conjecture), output_isabelle_annotated_formulae(Axioms), output_isabelle_annotated_formulae([Conjecture]), output_isabelle_trailer(Mode,Conjecture). isabelle(isabelle,Formulae,FileHeader):- !, isabelle(isabelle:sledgehammer,Formulae,FileHeader). %------------------------------------------------------------------------------ %---Information about the Isabelle format and file %------------------------------------------------------------------------------ isabelle_format_information('(*'-'*)','.thy'). isabelle_file_information(format,isabelle:[automodes],'Isabelle format'). %------------------------------------------------------------------------------