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

    Author: Walther Neuper, TU Graz

$ cd /usr/local/Isabelle2009-1/src/Pure/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"; 

*)

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"

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

*}

*)

(*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 ... *}*)

*)

end