neuper@37906: (*  Title:   ~~~/isac/Isac_Mathengine.thy
neuper@37906:     Author: Walther Neuper, TU Graz
neuper@37906: 
neuper@37910: $ cd /usr/local/Isabelle2009-1/src/Tools/isac
neuper@37906: $ /usr/local/isabisac/bin/isabelle emacs Isac_Mathengine.thy &
neuper@37906: $ /usr/local/isabisac/bin/isabelle jedit Isac_Mathengine.thy &
neuper@37906: 
neuper@37906: OR tty (unusable: after errors wrong toplevel):
neuper@37906: $ cd "/home/neuper/proto2/isac/src/sml"
neuper@37906: $ isabelle-process HOL HOL-Isac
neuper@37906: ML> use_thy "Isac_Mathengine"; 
neuper@37924: 
neuper@37924: 12345678901234567890123456789012345678901234567890123456789012345678901234567890
neuper@37924:         10        20        30        40        50        60        70        80
neuper@37906: *)
neuper@37906: 
neuper@37906: header {* Loading the isac mathengine *}
neuper@37906: 
neuper@37906: theory Isac_Mathengine
neuper@37906: (*imports Complex_Main*)
neuper@37906: imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)
neuper@37906: begin
neuper@37906: 
neuper@37906: ML {* Toplevel.debug := true; *}
neuper@37906: use "library.sml"
neuper@37906: use "calcelems.sml"
neuper@37906: ML {* check_guhs_unique := true *}
neuper@37906: 
neuper@37906: use "Scripts/term_G.sml"
neuper@37906: use "Scripts/calculate.sml"
neuper@37906: use "Scripts/rewrite.sml"
neuper@37906: use_thy"Scripts/Script"
neuper@37906: use "Scripts/scrtools.sml"
neuper@37906: 
neuper@37925: use "ME/mstools.sml"
neuper@37925: use "ME/ctree.sml"
neuper@37927: use "ME/ptyps.sml"
neuper@37928: use "ME/generate.sml"
neuper@37925: 
neuper@37924: ML {*
neuper@37928: thy2ctxt;
neuper@37924: *}
neuper@37924: 
neuper@37924: 
neuper@37928: 
neuper@37906: (*
neuper@37906: use "ME/calchead.sml"
neuper@37906: use "ME/appl.sml"
neuper@37906: use "ME/rewtools.sml"
neuper@37906: use "ME/script.sml"
neuper@37906: use "ME/solve.sml"
neuper@37906: use "ME/inform.sml"
neuper@37906: use "ME/mathengine.sml"
neuper@37906: 
neuper@37906: use "xmlsrc/mathml.sml"
neuper@37906: use "xmlsrc/datatypes.sml"
neuper@37906: use "xmlsrc/pbl-met-hierarchy.sml"
neuper@37906: use "xmlsrc/thy-hierarchy.sml" 
neuper@37906: use "xmlsrc/interface-xml.sml"
neuper@37906: 
neuper@37906: use "FE-interface/messages.sml"
neuper@37906: use "FE-interface/states.sml"
neuper@37906: use "FE-interface/interface.sml"
neuper@37906: 
neuper@37906: use "print_exn_G.sml"
neuper@37906: 
neuper@37906: text "**** build math-engine complete *************************"
neuper@37906: *)(*
neuper@37906: setup {*
neuper@37906:   Code_Preproc.setup
neuper@37906:   #> Code_ML.setup
neuper@37906:   #> Code_Haskell.setup
neuper@37906:   #> Nbe.setup
neuper@37906: *}
neuper@37906: *)
neuper@37906: 
neuper@37925: (*--------------------------shift to some isac-10 -------------------
neuper@37906: (*cleaner output from...*)
neuper@37906: ML_command {*
neuper@37906: "----- ";
neuper@37906: writeln "werwerw";
neuper@37906: *}
neuper@37906: 
neuper@37906: ML {* @{prop "False"} *}
neuper@37906: (*ML {* @{type "int"} *} only new version*)
neuper@37906: ML {* @{thm  conjI} *}
neuper@37906: ML {* @{thms  conjI TrueI} *}
neuper@37906: ML {* @{theory} *}
neuper@37906: 
neuper@37906: ML{* @{const_name plus} *} (*creates long names (extern names)*)
neuper@37906: term plus
neuper@37906: 
neuper@37906: term foo
neuper@37906: (*ML{* @{const_name foo} *}  only new version*)
neuper@37906:  
neuper@37906: text {*
neuper@37906: werwer
neuper@37906:  *}
neuper@37906: 
neuper@37906: ML {*
neuper@37906:   fun inc_by_five x =
neuper@37906:   x |> (fn x => x + 1)
neuper@37906: *}
neuper@37906: 
neuper@37906: (*canonical argument order introduced after 1997*)
neuper@37906: 
neuper@37906: text{*
neuper@37906: this is the most appropriate fold for lists (generalizes to lists of lists by (fold o fold o fold))
neuper@37906: @{ML fold}
neuper@37906: 
neuper@37906: @{ML fold_rev}
neuper@37906: 
neuper@37906: for accumulating side results in |>
neuper@37906: @{ML fold_map}
neuper@37906: *}
neuper@37906: 
neuper@37906: ML {* 
neuper@37906:   val items = 1 upto 10;
neuper@37906:   val l1 = fold cons items []; (*alternating useful frequently*)
neuper@37906: *}
neuper@37906: 
neuper@37906: ML{*
neuper@37906:   fun merge_list eq (xs, ys) = fold_rev (insert eq) ys xs;
neuper@37906: *}
neuper@37906: ML{*
neuper@37906:   merge_list (op =) ([3,2,1], [7,5,3,1]);
neuper@37906:   merge_list (op =) ([3,2,1], [7,5,3,1]);
neuper@37906: *}
neuper@37906: 
neuper@37906: (*session 2-------Christian+Makarius---------------*)
neuper@37906: ML{*
neuper@37906: let
neuper@37906:   val ctxt = @{context}
neuper@37906: in 1 end
neuper@37906: *}
neuper@37906: 
neuper@37906: (* build and handle tables THIS IS THE ACCESS-STRUCTURE...
neuper@37906: ML{*
neuper@37906:   structure Data = Theory_Data
neuper@37906:   (
neuper@37906:     type T = term Symtab.table
neuper@37906:     val empty = Symtab.empty
neuper@37906:     val extend = O
neuper@37906:     fun merge (t1, t2) = Symtab.merge (op = ) (t1, t2)
neuper@37906:   )
neuper@37906: *}
neuper@37906: *)
neuper@37906: (*session 3-------Blanchette--------------------
neuper@37906: working on nitpic, ML level tool
neuper@37906: 
neuper@37906: SEE THESE LECTURE NOTES !!!*)
neuper@37906: 
neuper@37906: (*
neuper@37906: ML{*
neuper@37906: Const ("x", dummyT) |> Syntax.check_term @{context}
neuper@37906:                        ^^^^^^^^^^^^^^^^^
neuper@37906: *}
neuper@37906: *)
neuper@37906: 
neuper@37906: text{*
neuper@37906: SEE funs for 
neuper@37906: # deleting identifiers
neuper@37906: # handle Bounds when made visible
neuper@37906: # kill trivial quantifiers, e.g. \foral x. (NO x)
neuper@37906: # handling name clashes in Abs
neuper@37906: # which constants, free vars ... occur in a term !!!!!!!!!!!
neuper@37906: # Var (("x", 2), dummyT)   ... 25 old from Larry "maxidx"
neuper@37906: # get fresh Const, Var
neuper@37906: # use the "Name" structure
neuper@37906: 
neuper@37906: *}
neuper@37906: 
neuper@37906: ML{* val context = Name.make_context ["d"] *}
neuper@37906: 
neuper@37906: (*
neuper@37906: ML{* Name.invents context "foo" 10  *}
neuper@37906: (*ML{* Name variants ... *}*)
neuper@37906: *)
neuper@37925: --------------------------shift to some isac-10 -------------------*)
neuper@37906: 
neuper@37906: end
neuper@37906: