walther@59632: (* Title: build the Isac-Kernel: MathEngine & Knowledge neuper@38057: Author: Walther Neuper, TU Graz, 100808 neuper@38051: (c) due to copyright terms neuper@38051: neuper@52062: For creating a heap image of isac see ~~/ROOT. walther@59632: For debugging see text at begin below, e.g. theory dependencies: walther@59632: ~$ evince file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf & neuper@52062: wneuper@59586: ATTENTION: no errors in this theory do not mean that there are no errors in Isac .. walther@59866: .. open theories collecting files from folders: BaseDefinitions.thy, ProgLang.thy etc. walther@59632: Errors are rigorously detected by isabelle build. neuper@37906: *) neuper@37906: walther@59998: theory Build_Isac wneuper@59206: imports walther@59887: (* theory Know_Store imports Complex_Main wenzelm@60192: $ISABELLE_ISAC/BaseDefinitions walther@59632: ML_file libraryC.sml walther@59865: ML_file theoryC.sml walther@59963: ML_file unparseC.sml walther@59850: ML_file "rule-def.sml" walther@59963: ML_file "thmC-def.sml" walther@59919: ML_file "eval-def.sml" walther@59858: ML_file "rewrite-order.sml" walther@59632: ML_file rule.sml walther@59963: ML_file "error-pattern-def.sml" walther@59852: ML_file "rule-set.sml" walther@59963: walther@59963: ML_file "store.sml" walther@59963: ML_file "check-unique.sml" walther@59963: ML_file "specification.sml" walther@59963: ML_file "model-pattern.sml" walther@59963: ML_file "problem-def.sml" walther@59963: ML_file "method-def.sml" walther@59963: ML_file "cas-def.sml" walther@59963: ML_file "thy-write.sml" walther@59887: theory BaseDefinitions imports Know_Store wenzelm@60192: $ISABELLE_ISAC/BaseDefinitions walther@59632: ML_file termC.sml walther@59963: ML_file substitution.sml walther@59632: ML_file contextC.sml walther@59687: ML_file environment.sml walther@60077: ( ** ) "BaseDefinitions/BaseDefinitions"( **) walther@60317: (* Walther@60516: theory Calc_Binop imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions" walther@60317: at $ISABELLE_ISAC/ProgLang walther@59902: ML_file evaluate.sml wenzelm@60192: theory ListC imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions" wenzelm@60192: theory Program imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions" Walther@60516: theory Prog_Expr imports Calc_Binop ListC Program walther@60317: theory Prog_Tac imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions" wenzelm@60192: theory Tactical imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions" walther@60317: theory Auto_Prog imports Prog_Tac Tactical walther@59632: theory ProgLang imports Prog_Expr Auto_Prog walther@60317: at $ISABELLE_ISAC/ProgLang walther@60077: ( ** ) "ProgLang/ProgLang"( **) wneuper@59600: (* walther@59674: theory MathEngBasic imports wenzelm@60192: "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript" walther@60317: at $ISABELLE_ISAC/MathEngBasic walther@59875: ML_file thmC.sml walther@59963: ML_file problem.sml walther@59963: ML_file method.sml walther@59963: ML_file "cas-command.sml" walther@59963: walther@59865: ML_file rewrite.sml walther@59963: walther@59963: ML_file "model-def.sml" walther@59963: ML_file "istate-def.sml" walther@59674: ML_file "calc-tree-elem.sml" walther@59963: ML_file "pre-conds-def.sml" walther@59963: walther@59632: ML_file tactic.sml walther@59963: ML_file applicable.sml walther@59963: walther@59777: ML_file position.sml walther@59674: ML_file "ctree-basic.sml" walther@59674: ML_file "ctree-access.sml" walther@59674: ML_file "ctree-navi.sml" walther@59674: ML_file ctree.sml walther@59963: walther@59963: ML_file "state-steps.sml" walther@59777: ML_file calculation.sml walther@60077: ( ** ) "MathEngBasic/MathEngBasic"( **) walther@59674: (* wenzelm@60192: theory Input_Descript imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions" wenzelm@60192: $ISABELLE_ISAC/Specify wenzelm@60192: theory Specify imports "$ISABELLE_ISAC/ProgLang/ProgLang" Input_Descript wenzelm@60192: $ISABELLE_ISAC/Specify walther@59963: ML_file formalise.sml walther@59963: ML_file "o-model.sml" walther@59963: ML_file "i-model.sml" walther@59963: ML_file "p-model.sml" walther@59963: ML_file model.sml walther@59963: ML_file "pre-conditions.sml" walther@59963: ML_file refine.sml walther@59963: ML_file "mstools.sml" (*..TODO review*) walther@59963: ML_file ptyps.sml (*..TODO review*) walther@59963: ML_file "test-out.sml" walther@59963: ML_file "specify-step.sml" walther@59963: ML_file calchead.sml (*..TODO review*) walther@59963: ML_file "input-calchead.sml" walther@59777: ML_file "step-specify.sml" walther@59777: ML_file specify.sml walther@60077: ( ** ) "Specify/Specify"( **) wneuper@59600: (* wenzelm@60192: theory Interpret imports "$ISABELLE_ISAC/Specify/Specify" wenzelm@60192: $ISABELLE_ISAC/Interpret walther@59777: ML_file istate.sml walther@59963: ML_file "sub-problem.sml" walther@59963: ML_file "thy-read.sml" walther@59963: ML_file "solve-step.sml" walther@59963: ML_file "error-pattern.sml" walther@59963: ML_file derive.sml walther@59794: ML_file "li-tool.sml" walther@59632: ML_file "lucas-interpreter.sml" walther@59794: ML_file "step-solve.sml" walther@60077: ( ** ) "Interpret/Interpret"( **) wneuper@59600: (* walther@60077: theory MathEngine imports Interpret.Interpret wenzelm@60192: $ISABELLE_ISAC/MathEngine walther@59833: ML_file "fetch-tactics.sml" walther@59632: ML_file solve.sml walther@59794: ML_file step.sml walther@59833: ML_file "detail-step.sml" walther@59634: ML_file "mathengine-stateless.sml" walther@59632: ML_file messages.sml walther@59632: ML_file states.sml walther@60077: ( ** ) "MathEngine/MathEngine"( **) wneuper@59600: (* wenzelm@60192: theory Test_Code imports "$ISABELLE_ISAC/MathEngine/MathEngine" wenzelm@60192: $ISABELLE_ISAC/Test_Code walther@59814: ML_file "test-code.sml" walther@60077: ( ** ) "Test_Code/Test_Code"( **) walther@59814: (* wenzelm@60192: theory BridgeLibisabelle imports "$ISABELLE_ISAC/MathEngine/MathEngine" wenzelm@60192: $ISABELLE_ISAC/BridgeLibisabelle walther@59963: ML_file "thy-present.sml" walther@59963: ML_file mathml.sml walther@59632: ML_file datatypes.sml walther@59632: ML_file "pbl-met-hierarchy.sml" walther@59632: ML_file "thy-hierarchy.sml" walther@59632: ML_file "interface-xml.sml" walther@59632: ML_file interface.sml walther@60077: ( ** ) "BridgeLibisabelle/BridgeLibisabelle"( **) walther@60044: (* walther@60181: theory Calculation imports Calculation (*preliminary for starting Isabelle/Isac*) wenzelm@60192: $ISABELLE_ISAC/BridgeJEdit walther@60181: ML_file parseC.sml walther@60181: ML_file preliminary.sml walther@60181: theory BridgeJEdit imports Calculation (*preliminary for starting Isabelle/Isac*) wenzelm@60192: $ISABELLE_ISAC/BridgeJEdit walther@60181: ( ** ) "BridgeLibisabelle/BridgeLibisabelle"( **) walther@60181: (* wenzelm@60192: theory Isac imports "$ISABELLE_ISAC/MathEngine/MathEngine" walther@60044: ML_file parseC.sml walther@60044: theory BridgeJEdit imports Isac walther@60149: ( **) "BridgeJEdit/BridgeJEdit" (*DEactivate after devel.of BridgeJEdit*) wneuper@59147: walther@59612: "Knowledge/Build_Thydata" (*imports Isac.thy etc*) wneuper@59469: wneuper@59601: (*//-----------------------------------------------------------------------------------------\\*) wneuper@59601: (*\\-----------------------------------------------------------------------------------------//*) neuper@48763: begin Walther@60566: ML \ Walther@60566: \ ML \ Walther@60566: \ ML \ Walther@60566: \ neuper@48760: wneuper@59472: text \ neuper@55276: show theory dependencies using the graph browser, neuper@55276: open "browser_info/HOL/Isac/session.graph" neuper@55276: and proceed from the ancestors towards the siblings. wneuper@59472: \ neuper@55276: wneuper@59472: section \check presence of definitions from directories\ neuper@48763: wneuper@59263: (*declare [[ML_print_depth = 999]]*) walther@59902: ML \Eval.adhoc_thm; (*from "ProgLang/evaluate.sml" *)\ wneuper@59472: ML \Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\ walther@59953: ML \Input_Descript.for_real_list; (*from "Input_Descript.thy" *)\ Walther@60557: ML \(*Test_Code.me;*)\ walther@59613: text \contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\ walther@59801: ML \prog_expr\ wneuper@59562: walther@59603: ML \Prog_Expr.eval_occurs_in\ walther@59603: ML \@{thm last_thmI}\ walther@60077: (** )ML \@{thm Querkraft_Belastung}\( *exception FAIL NONE raised (line 161 of "General/scan.ML")*) neuper@41905: Walther@60502: declare [[check_unique = false]] wneuper@59472: ML \writeln "**** isac kernel = math-engine + Knowledge complete ******"\ wneuper@59592: ML \@{theory "Isac_Knowledge"}\ wneuper@59472: ML \(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"] walther@59997: ERROR: app_py: not found: ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]*)\ neuper@42412: wneuper@59472: section \State of approaching Isabelle by Isac\ wneuper@59472: text \ Walther@60551: Mathias Lehnfeld gives the following list in his thesis in section neuper@55431: 4.2.3 Relation to Ongoing Isabelle Development. wneuper@59472: \ wneuper@59472: subsection \(0) Survey on remaining Unsynchronized.ref\ wneuper@59472: text \ Walther@60507: DONE wneuper@59472: \ wneuper@59472: subsection \(1) Exploit parallelism for concurrent session management\ wneuper@59472: subsection \(2) Make Isac’s programming language usable\ wneuper@59472: subsection \(3) Adopt Isabelle’s numeral computation for Isac\ wneuper@59472: text \ neuper@55431: In 2002 isac already strived for floating point numbers. Since that time neuper@55431: isac represents numerals as "Free", see below (*1*). These experiments are neuper@55431: unsatisfactory with respect to logical soundness. neuper@55431: Since Isabelle now has started to care about floating point numbers, it is high neuper@55431: time to adopt these together with the other numerals. Isabelle2012/13's numerals wenzelm@60217: are different from Isabelle2011, see "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/termC.sml". neuper@55431: neuper@55431: The transition from "Free" to standard numerals is a task to be scheduled for neuper@55431: several weeks. The urgency of this task follows from the experience, neuper@55431: that (1.2) for "thehier" is very hard, because "num_str" seems to destroy neuper@55431: some of the long identifiers of theorems which would tremendously simplify neuper@55431: building a hierarchy of theorems according to (1.2), see (*2*) below. wneuper@59472: \ wneuper@59472: ML \(*1*) Free ("123.456", HOLogic.realT)\ neuper@55484: wneuper@59472: subsection \(4) Improve the efficiency of Isac’s rewrite-engine\ wneuper@59472: subsection \(5) Adopt Isabelle/jEdit for Isac\ neuper@55431: neuper@37906: end