1 (* Title: ~~~/isac/Isac_Mathengine.thy
2 Author: Walther Neuper, TU Graz
4 $ cd /usr/local/Isabelle2009-1/src/Pure/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";
14 header {* Loading the isac mathengine *}
16 theory Isac_Mathengine
17 (*imports Complex_Main*)
18 imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)
21 ML {* Toplevel.debug := true; *}
25 ML {* check_guhs_unique := true *}
27 use "Scripts/term_G.sml"
28 use "Scripts/calculate.sml"
30 use "Scripts/rewrite.sml"
31 use_thy"Scripts/Script"
33 use "Scripts/scrtools.sml"
46 use "ME/mathengine.sml"
48 use "xmlsrc/mathml.sml"
49 use "xmlsrc/datatypes.sml"
50 use "xmlsrc/pbl-met-hierarchy.sml"
51 use "xmlsrc/thy-hierarchy.sml"
52 use "xmlsrc/interface-xml.sml"
54 use "FE-interface/messages.sml"
55 use "FE-interface/states.sml"
56 use "FE-interface/interface.sml"
60 text "**** build math-engine complete *************************"
71 (*cleaner output from...*)
77 ML {* @{prop "False"} *}
78 (*ML {* @{type "int"} *} only new version*)
80 ML {* @{thms conjI TrueI} *}
83 ML{* @{const_name plus} *} (*creates long names (extern names)*)
87 (*ML{* @{const_name foo} *} only new version*)
98 (*canonical argument order introduced after 1997*)
101 this is the most appropriate fold for lists (generalizes to lists of lists by (fold o fold o fold))
106 for accumulating side results in |>
111 val items = 1 upto 10;
112 val l1 = fold cons items []; (*alternating useful frequently*)
116 fun merge_list eq (xs, ys) = fold_rev (insert eq) ys xs;
119 merge_list (op =) ([3,2,1], [7,5,3,1]);
120 merge_list (op =) ([3,2,1], [7,5,3,1]);
123 (*session 2-------Christian+Makarius---------------*)
126 val ctxt = @{context}
130 (* build and handle tables THIS IS THE ACCESS-STRUCTURE...
132 structure Data = Theory_Data
134 type T = term Symtab.table
135 val empty = Symtab.empty
137 fun merge (t1, t2) = Symtab.merge (op = ) (t1, t2)
141 (*session 3-------Blanchette--------------------
142 working on nitpic, ML level tool
144 SEE THESE LECTURE NOTES !!!*)
148 Const ("x", dummyT) |> Syntax.check_term @{context}
155 # deleting identifiers
156 # handle Bounds when made visible
157 # kill trivial quantifiers, e.g. \foral x. (NO x)
158 # handling name clashes in Abs
159 # which constants, free vars ... occur in a term !!!!!!!!!!!
160 # Var (("x", 2), dummyT) ... 25 old from Larry "maxidx"
161 # get fresh Const, Var
162 # use the "Name" structure
166 ML{* val context = Name.make_context ["d"] *}
169 ML{* Name.invents context "foo" 10 *}
170 (*ML{* Name variants ... *}*)