(*  Title:   ~~~/isac/Isac_Mathengine.thy

     Author: Walther Neuper, TU Graz

 $ cd /usr/local/Isabelle2009-1/src/Tools/isac

 $ /usr/local/isabisac/bin/isabelle emacs Isac_Mathengine.thy &

 $ /usr/local/isabisac/bin/isabelle jedit Isac_Mathengine.thy &

 OR tty (unusable: after errors wrong toplevel):

 $ cd "/home/neuper/proto2/isac/src/sml"

 $ isabelle-process HOL HOL-Isac

 ML> use_thy "Isac_Mathengine"; 

 12345678901234567890123456789012345678901234567890123456789012345678901234567890

         10        20        30        40        50        60        70        80

 *)

 header {* Loading the isac mathengine *}

 theory Isac_Mathengine

 (*imports Complex_Main*)

 imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)

 begin

 ML {* Toplevel.debug := true; *}

 use "library.sml"

 use "calcelems.sml"

 ML {* check_guhs_unique := true *}

 use "Scripts/term_G.sml"

 use "Scripts/calculate.sml"

 use "Scripts/rewrite.sml"

 use_thy"Scripts/Script"

 use "Scripts/scrtools.sml"

 use "ME/mstools.sml"

 use "ME/ctree.sml"

 use "ME/ptyps.sml"

 ML {*

 member;

 @{term 111};

 *}

 (*

 use "ME/generate.sml"

 use "ME/calchead.sml"

 use "ME/appl.sml"

 use "ME/rewtools.sml"

 use "ME/script.sml"

 use "ME/solve.sml"

 use "ME/inform.sml"

 use "ME/mathengine.sml"

 use "xmlsrc/mathml.sml"

 use "xmlsrc/datatypes.sml"

 use "xmlsrc/pbl-met-hierarchy.sml"

 use "xmlsrc/thy-hierarchy.sml" 

 use "xmlsrc/interface-xml.sml"

 use "FE-interface/messages.sml"

 use "FE-interface/states.sml"

 use "FE-interface/interface.sml"

 use "print_exn_G.sml"

 text "**** build math-engine complete *************************"

 *)(*

 setup {*

   Code_Preproc.setup

   #> Code_ML.setup

   #> Code_Haskell.setup

   #> Nbe.setup

 *}

 *)

 (*--------------------------shift to some isac-10 -------------------

 (*cleaner output from...*)

 ML_command {*

 "----- ";

 writeln "werwerw";

 *}

 ML {* @{prop "False"} *}

 (*ML {* @{type "int"} *} only new version*)

 ML {* @{thm  conjI} *}

 ML {* @{thms  conjI TrueI} *}

 ML {* @{theory} *}

 ML{* @{const_name plus} *} (*creates long names (extern names)*)

 term plus

 term foo

 (*ML{* @{const_name foo} *}  only new version*)

 text {*

 werwer

  *}

 ML {*

   fun inc_by_five x =

   x |> (fn x => x + 1)

 *}

 (*canonical argument order introduced after 1997*)

 text{*

 this is the most appropriate fold for lists (generalizes to lists of lists by (fold o fold o fold))

 @{ML fold}

 @{ML fold_rev}

 for accumulating side results in |>

 @{ML fold_map}

 *}

 ML {* 

   val items = 1 upto 10;

   val l1 = fold cons items []; (*alternating useful frequently*)

 *}

 ML{*

   fun merge_list eq (xs, ys) = fold_rev (insert eq) ys xs;

 *}

 ML{*

   merge_list (op =) ([3,2,1], [7,5,3,1]);

   merge_list (op =) ([3,2,1], [7,5,3,1]);

 *}

 (*session 2-------Christian+Makarius---------------*)

 ML{*

 let

   val ctxt = @{context}

 in 1 end

 *}

 (* build and handle tables THIS IS THE ACCESS-STRUCTURE...

 ML{*

   structure Data = Theory_Data

   (

     type T = term Symtab.table

     val empty = Symtab.empty

     val extend = O

     fun merge (t1, t2) = Symtab.merge (op = ) (t1, t2)

   )

 *}

 *)

 (*session 3-------Blanchette--------------------

 working on nitpic, ML level tool

 SEE THESE LECTURE NOTES !!!*)

 (*

 ML{*

 Const ("x", dummyT) |> Syntax.check_term @{context}

                        ^^^^^^^^^^^^^^^^^

 *}

 *)

 text{*

 SEE funs for 

 # deleting identifiers

 # handle Bounds when made visible

 # kill trivial quantifiers, e.g. \foral x. (NO x)

 # handling name clashes in Abs

 # which constants, free vars ... occur in a term !!!!!!!!!!!

 # Var (("x", 2), dummyT)   ... 25 old from Larry "maxidx"

 # get fresh Const, Var

 # use the "Name" structure

 *}

 ML{* val context = Name.make_context ["d"] *}

 (*

 ML{* Name.invents context "foo" 10  *}

 (*ML{* Name variants ... *}*)

 *)

 --------------------------shift to some isac-10 -------------------*)

 end