
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 \<open>
Walther@60566: \<close> ML \<open>
Walther@60566: \<close> ML \<open>
Walther@60566: \<close> 
neuper@48760: 
wneuper@59472: text \<open>
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: \<close>
neuper@55276: 
wneuper@59472: section \<open>check presence of definitions from directories\<close>
neuper@48763: 
wneuper@59263: (*declare [[ML_print_depth = 999]]*)
walther@59902: ML \<open>Eval.adhoc_thm; (*from "ProgLang/evaluate.sml" *)\<close>
wneuper@59472: ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
walther@59953: ML \<open>Input_Descript.for_real_list; (*from "Input_Descript.thy" *)\<close>
Walther@60557: ML \<open>(*Test_Code.me;*)\<close>
walther@59613: text \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close>
walther@59801: ML \<open>prog_expr\<close>
wneuper@59562:                                                          
walther@59603: ML \<open>Prog_Expr.eval_occurs_in\<close>
walther@59603: ML \<open>@{thm last_thmI}\<close>
walther@60077: (** )ML \<open>@{thm Querkraft_Belastung}\<close>( *exception FAIL NONE raised (line 161 of "General/scan.ML")*)
neuper@41905: 
Walther@60502: declare [[check_unique = false]]
wneuper@59472: ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close>
wneuper@59592: ML \<open>@{theory "Isac_Knowledge"}\<close>
wneuper@59472: ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
walther@59997:   ERROR: app_py: not found: ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]*)\<close>
neuper@42412: 
wneuper@59472: section \<open>State of approaching Isabelle by Isac\<close>
wneuper@59472: text \<open>
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: \<close>
wneuper@59472: subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close>
wneuper@59472: text \<open>
Walther@60507:   DONE
wneuper@59472: \<close>
wneuper@59472: subsection \<open>(1) Exploit parallelism for concurrent session management\<close>
wneuper@59472: subsection \<open>(2) Make Isac’s programming language usable\<close>
wneuper@59472: subsection \<open>(3) Adopt Isabelle’s numeral computation for Isac\<close>
wneuper@59472: text \<open>
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: \<close>
wneuper@59472: ML \<open>(*1*) Free ("123.456", HOLogic.realT)\<close>
neuper@55484: 
wneuper@59472: subsection \<open>(4) Improve the efficiency of Isac’s rewrite-engine\<close>
wneuper@59472: subsection \<open>(5) Adopt Isabelle/jEdit for Isac\<close>
neuper@55431: 
neuper@37906: end




