IsaProve.hs revision 7bd5754e08c0e163f96fff840189a38394f96af0
4e5b757fbcf21077677360be274461dcd9064106kupferModule : $Header$
4e5b757fbcf21077677360be274461dcd9064106kupferCopyright : (c) University of Cambridge, Cambridge, England
4e5b757fbcf21077677360be274461dcd9064106kupfer adaption (c) Till Mossakowski, Uni Bremen 2002-2004
4e5b757fbcf21077677360be274461dcd9064106kupferLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
4e5b757fbcf21077677360be274461dcd9064106kupferMaintainer : hets@tzi.de
4e5b757fbcf21077677360be274461dcd9064106kupferStability : provisional
4e5b757fbcf21077677360be274461dcd9064106kupferPortability : portable
4e5b757fbcf21077677360be274461dcd9064106kupfer Interface for Isabelle theorem prover.
4e5b757fbcf21077677360be274461dcd9064106kupfer todo: thy files in subdir
4e5b757fbcf21077677360be274461dcd9064106kupfer Interface between Isabelle and Hets:
4e5b757fbcf21077677360be274461dcd9064106kupfer Hets writes Isabelle .thy file and opens window with button (GUI/HTkUtils.hs, uni/htk/test, ask cxl)
4e5b757fbcf21077677360be274461dcd9064106kupfer User extends .thy file with proofs
4e5b757fbcf21077677360be274461dcd9064106kupfer User presses button
4e5b757fbcf21077677360be274461dcd9064106kupfer Hets reads in user-modified .thy file
4e5b757fbcf21077677360be274461dcd9064106kupfer Hets write new .thy file (different name), consisting of
4e5b757fbcf21077677360be274461dcd9064106kupfer - original theory (i.e. put theory string into variable)
4e5b757fbcf21077677360be274461dcd9064106kupfer - proof part of user-modified file (look for first "\ntheorem")
4e5b757fbcf21077677360be274461dcd9064106kupfer - ML code for check_theorem
4e5b757fbcf21077677360be274461dcd9064106kupfer - ML "check_theorem \"name1\" \"theorem1\" name.thy" (name: thName)
4e5b757fbcf21077677360be274461dcd9064106kupfer - ML "check_theorem \"namen\" "\theoremn\" name.thy"
4e5b757fbcf21077677360be274461dcd9064106kupfer Hets runs new .thy file in Isar batch mode (system " .... ")
4e5b757fbcf21077677360be274461dcd9064106kupfer Hets inspects log file and extracts proven theorems
4e5b757fbcf21077677360be274461dcd9064106kupfer fun check_theorem name thm thy =
aconv(#prop(rep_thm(Drule.freeze_all(get_thm thy name))), snd(read_axm (sign_of thy) (name,thm)))
module Isabelle.IsaProve where
import Logic.Prover
import Isabelle.IsaSign
import Isabelle.IsaPrint
import Isabelle.Translate
import Common.AS_Annotation
import Common.PrettyPrint
import Data.List
import Data.Maybe
import Debug.Trace
-- system (isabelle ++ "/isabelle -e "++newThy++" -q HOL" ++ " heap.isa")
origName = thName'++".orig.thy"
provedName = thName'++"_proved.thy"
++ "aconv(#prop(rep_thm(Drule.freeze_all(get_thm thy name))),"
thyPath = "ML \"val hetsLib = (OS.Process.getEnv \\\"HETS_LIB\\\"); \n"
map nameSen (zip sens [1..length sens])