1 (* Title: ~~~/isac/Isac_Mathengine.thy
2 Author: Walther Neuper, TU Graz
4 $ cd /usr/local/Isabelle2009-1/src/Tools/isac
5 $ /usr/local/isabisac/bin/isabelle emacs Isac_Mathengine.thy &
6 $ /usr/local/isabisac/bin/isabelle jedit Isac_Mathengine.thy &
8 OR tty (unusable: after errors wrong toplevel):
9 $ cd "/home/neuper/proto2/isac/src/sml"
10 $ isabelle-process HOL HOL-Isac
11 ML> use_thy "Isac_Mathengine";
13 12345678901234567890123456789012345678901234567890123456789012345678901234567890
14 10 20 30 40 50 60 70 80
17 header {* Loading the isac mathengine *}
19 theory Isac_Mathengine
20 (*imports Complex_Main*)
21 imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)
24 ML {* Toplevel.debug := true; *}
28 ML {* check_guhs_unique := true *}
30 use "Scripts/term_G.sml"
31 use "Scripts/calculate.sml"
32 use "Scripts/rewrite.sml"
33 use_thy"Scripts/Script"
34 use "Scripts/scrtools.sml"
56 use "ME/mathengine.sml"
58 use "xmlsrc/mathml.sml"
59 use "xmlsrc/datatypes.sml"
60 use "xmlsrc/pbl-met-hierarchy.sml"
61 use "xmlsrc/thy-hierarchy.sml"
62 use "xmlsrc/interface-xml.sml"
64 use "FE-interface/messages.sml"
65 use "FE-interface/states.sml"
66 use "FE-interface/interface.sml"
70 text "**** build math-engine complete *************************"
81 (*cleaner output from...*)
87 ML {* @{prop "False"} *}
88 (*ML {* @{type "int"} *} only new version*)
90 ML {* @{thms conjI TrueI} *}
93 ML{* @{const_name plus} *} (*creates long names (extern names)*)
97 (*ML{* @{const_name foo} *} only new version*)
108 (*canonical argument order introduced after 1997*)
111 this is the most appropriate fold for lists (generalizes to lists of lists by (fold o fold o fold))
116 for accumulating side results in |>
121 val items = 1 upto 10;
122 val l1 = fold cons items []; (*alternating useful frequently*)
126 fun merge_list eq (xs, ys) = fold_rev (insert eq) ys xs;
129 merge_list (op =) ([3,2,1], [7,5,3,1]);
130 merge_list (op =) ([3,2,1], [7,5,3,1]);
133 (*session 2-------Christian+Makarius---------------*)
136 val ctxt = @{context}
140 (* build and handle tables THIS IS THE ACCESS-STRUCTURE...
142 structure Data = Theory_Data
144 type T = term Symtab.table
145 val empty = Symtab.empty
147 fun merge (t1, t2) = Symtab.merge (op = ) (t1, t2)
151 (*session 3-------Blanchette--------------------
152 working on nitpic, ML level tool
154 SEE THESE LECTURE NOTES !!!*)
158 Const ("x", dummyT) |> Syntax.check_term @{context}
165 # deleting identifiers
166 # handle Bounds when made visible
167 # kill trivial quantifiers, e.g. \foral x. (NO x)
168 # handling name clashes in Abs
169 # which constants, free vars ... occur in a term !!!!!!!!!!!
170 # Var (("x", 2), dummyT) ... 25 old from Larry "maxidx"
171 # get fresh Const, Var
172 # use the "Name" structure
176 ML{* val context = Name.make_context ["d"] *}
179 ML{* Name.invents context "foo" 10 *}
180 (*ML{* Name variants ... *}*)